Slot-zero phase anchors for the incoming R-324 Fourier branch

After the incoming endpoint is Fourier-integrated, its character is anchored at the sparse successor of production slot zero. This file records the exact one-head geometry of that anchor. A head whose predecessor is not slot zero leaves the anchor in the post coordinates; a head whose predecessor is slot zero moves it from the first head coordinate to the post-collapse successor point.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.incomingPhaseAnchor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (x y : T4) (v : res.SurvivingCoordinate → T4) : T4

Spatial point carrying the incoming Fourier character at a reachable within-half residual prefix.

Equations

• res.incomingPhaseAnchor x y v = Anderson4D.assemble x y (res.reconstruct v) (res.edgeSuccessor 0)

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingPhaseAnchor_reconstruct_split_eq_headFirst {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.incomingPhaseAnchor x y ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)) = t ⟨0, ⋯⟩

If the current head is fed by slot zero, the pre-collapse phase anchor is its first standard block coordinate.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingPhaseAnchor_afterHead_eq_headSuccessorPoint {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (x y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : (res.afterHead head tail hremaining).incomingPhaseAnchor x y v = res.headSuccessorPoint head tail hremaining x y v

When slot zero is absorbed, its post-collapse phase anchor is exactly the successor point used by the local primitive kernel.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingPhaseAnchor_reconstruct_split_eq_afterHead {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head ≠ 0) (x y : T4) (t : Fin (2 * residualBlockOrder head.2) → T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.incomingPhaseAnchor x y ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)) = (res.afterHead head tail hremaining).incomingPhaseAnchor x y v

A head not fed by slot zero leaves the incoming phase anchor entirely in the post-head coordinates.