Transport of the R-324 within-half predecessor

After an adjacent analytic prefix block is collapsed, the predecessor of the next block is the slot updated by that collapse. The slot is recomputed from the surviving active carrier; it is not the original production slot.

theorem Anderson4D.r324WithinHalfPredecessorSlot_mem {m : ℕ} (state : R324WithinHalfEdgeState m) (step : R322ExtractionStep m) : r324WithinHalfPredecessorSlot state step ∈ r324WithinHalfPredecessorCandidates state step

theorem Anderson4D.r324WithinHalfCandidate_le_predecessorSlot {m : ℕ} (state : R324WithinHalfEdgeState m) (step : R322ExtractionStep m) (edge : Fin (m + 1)) (hedge : edge ∈ r324WithinHalfPredecessorCandidates state step) : edge ≤ r324WithinHalfPredecessorSlot state step

theorem Anderson4D.R324WithinHalfStepContext.predecessorSlot_absorb_eq_of_adjacent {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (selected : R322ExtractionStep m) (hadjacent : ↑ctx.step.1.2 + 1 = ↑selected.1.1) (ρ : SmoothCutoff) (lam ε : ℝ) : r324WithinHalfPredecessorSlot (ctx.absorb ρ lam ε) selected = r324WithinHalfPredecessorSlot ctx.state ctx.step

The slot updated by an analytic prefix step is exactly the surviving predecessor slot of a block beginning immediately after it.

theorem Anderson4D.exists_r324WithinHalfState_of_schedule_prefix {m : ℕ} (pairing : PartialPairing (Fin m)) (ρ : SmoothCutoff) (lam ε : ℝ) (pre suffix : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule pairing = pre ++ suffix) : ∃ (state : R324WithinHalfEdgeState m), R324WithinHalfStateReachable pairing ρ lam ε state ∧ state.processed = pre

Every genuine prefix of the analytic schedule generates a reachable heterogeneous state. This is an induction on the prefix itself, rather than an arbitrary sequence of certified blocks.

theorem Anderson4D.exists_r324WithinHalf_nonemptyPrefix_predecessor_read {m : ℕ} (pairing : PartialPairing (Fin m)) (ρ : SmoothCutoff) (lam ε : ℝ) (prior : List (R322ExtractionStep m)) (prefixStep selected : R322ExtractionStep m) (suffix : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule pairing = prior ++ [prefixStep] ++ selected :: suffix) (hadjacent : ↑prefixStep.1.2 + 1 = ↑selected.1.1) : ∃ (ctx : R324WithinHalfStepContext pairing), R324WithinHalfStateReachable pairing ρ lam ε ctx.state ∧ ctx.state.processed = prior ∧ ctx.step = prefixStep ∧ ctx.suffix = selected :: suffix ∧ R324WithinHalfStateReachable pairing ρ lam ε (ctx.absorb ρ lam ε) ∧ (ctx.absorb ρ lam ε).processed = prior ++ [prefixStep] ∧ (ctx.absorb ρ lam ε).edges (r324WithinHalfPredecessorSlot (ctx.absorb ρ lam ε) selected) = ctx.collapsedKernel ρ lam ε

For a nonempty analytic prefix whose last block is adjacent to the selected block, the selected predecessor reads the edge produced by the last genuine collapse.