Post-prefix state at the R-324 first-left block

This file combines the genuine analytic-schedule decomposition with the heterogeneous edge-state iteration. Its headline concerns the processed state after integrating the prefix. It does not identify that state pointwise with the original unprocessed production integrand.

theorem Anderson4D.exists_r324FirstLeft_postPrefixState_predecessor_read {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ρ : SmoothCutoff) (lam ε : ℝ) (hextracted : r324FirstLeftPredecessorEdge e₀ hleft ∈ extractedRightEdges e₀.fst) : ∃ (prior : List (R322ExtractionStep m)) (step : R322ExtractionStep m) (post : List (R322ExtractionStep m)) (ctx : R324WithinHalfStepContext e₀.fst), r322AnalyticSchedule e₀.fst = prior ++ [step] ++ r324FirstLeftSelectedStep e₀ hleft :: post ∧ extractedRightEdge step.1 = r324FirstLeftPredecessorEdge e₀ hleft ∧ ctx.state.processed = prior ∧ ctx.step = step ∧ ctx.suffix = r324FirstLeftSelectedStep e₀ hleft :: post ∧ R324WithinHalfStateReachable e₀.fst ρ lam ε ctx.state ∧ R324WithinHalfStateReachable e₀.fst ρ lam ε (ctx.absorb ρ lam ε) ∧ (ctx.absorb ρ lam ε).processed = prior ++ [step] ∧ r324WithinHalfPredecessorSlot (ctx.absorb ρ lam ε) (r324FirstLeftSelectedStep e₀ hleft) = r324WithinHalfPredecessorSlot ctx.state ctx.step ∧ (ctx.absorb ρ lam ε).edges (r324WithinHalfPredecessorSlot (ctx.absorb ρ lam ε) (r324FirstLeftSelectedStep e₀ hleft)) = ctx.collapsedKernel ρ lam ε

If the production predecessor is extracted, the genuine analytic prefix produces a reachable state in which the selected block reads the three-kernel collapse stored by the last prefix step.