Reachability along the genuine R-322 proper prefix

Every proper prefix of the paper-ordered analytic schedule generates an actual heterogeneous edge state. The construction iterates the signed three-kernel update recorded by R322AnalyticAbsorbedState; it does not identify an unintegrated production integrand pointwise with the resulting state.

theorem Anderson4D.exists_r322AnalyticAbsorbedState_of_properPrefix {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (lam ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (pre suffix : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = pre ++ suffix) (hproper : ∀ step ∈ pre, step.1 ≠ r322WholeEndpoint q hq) : ∃ (state : R322AnalyticEdgeState q hq), R322AnalyticAbsorbedState ρ lam ε hq κ hκ state ∧ state.processed = pre

A genuine proper prefix of the analytic schedule produces a reachable heterogeneous state whose processed history is exactly that prefix.

theorem Anderson4D.exists_r322AnalyticReachableTerminalContext {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (lam ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) : ∃ (ctx : R322AnalyticTerminalStepContext q hq), R322AnalyticAbsorbedState ρ lam ε hq κ hκ ctx.state

The proper-prefix/terminal decomposition therefore reaches a certified terminal context on the actual heterogeneous edge state.