Incoming-endpoint independence at an R-324 head collapse

When the left endpoint of the current analytic head is the first internal vertex, its sparse predecessor is the incoming external slot. This file records the concrete geometry needed to Fourier-integrate that external variable before the head is absorbed:

• the named predecessor point is the incoming endpoint;
• the outgoing successor point is independent of that endpoint; and
• every factor outside the local head is independent of that endpoint.

All statements unfold the existing sparse residual integrand. No analytic collapse or Fubini hypothesis is introduced here.

theorem Anderson4D.R324WithinHalfResidualPrefix.predecessorSlot_eq_zero_of_head_left_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (hleft : ↑head.1.1 = 0) : r324WithinHalfPredecessorSlot res.state head = 0

A head beginning at the first internal vertex necessarily has the incoming external slot as sparse predecessor.

theorem Anderson4D.R324WithinHalfResidualPrefix.headPredecessorPoint_eq_incoming_of_head_left_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hleft : ↑head.1.1 = 0) (x y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.headPredecessorPoint head tail hremaining x y v = x

For a head beginning at internal vertex zero, the named predecessor point is literally the incoming external endpoint.

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

The outgoing successor point of any head is independent of the incoming external endpoint. This is stronger than the zero-left-endpoint case: the sparse successor lies strictly after an internal outgoing slot.

theorem Anderson4D.R324WithinHalfResidualPrefix.headOuterChainProductAfter_eq_of_incoming_endpoint_of_head_left_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hleft : ↑head.1.1 = 0) (x x' y : T4) (v : Fin m → T4) : res.headOuterChainProductAfter head tail hremaining x y v = res.headOuterChainProductAfter head tail hremaining x' y v

Once the head predecessor is slot zero, every post-collapse ordinary chain factor outside the local head is independent of the incoming external endpoint.

theorem Anderson4D.R324WithinHalfResidualPrefix.headOuterFactor_eq_of_incoming_endpoint_of_head_left_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hleft : ↑head.1.1 = 0) (x x' y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : res.headOuterFactor head tail hremaining ρ ε x y v = res.headOuterFactor head tail hremaining ρ ε x' y v

Every factor outside a zero-left-endpoint local head is independent of the incoming external endpoint. In particular, the outer factor may be held constant during the incoming Fourier integral.