Ordinary one-head transport of an incoming Fourier phase

Once the incoming endpoint has been Fourier-integrated, its character is carried by the sparse successor of slot zero. If a later primitive head is not fed by slot zero, that anchor is entirely a post-head coordinate. The existing weighted one-head collapse therefore applies verbatim with the character included in the post outer factor.

Weighted local sections

theorem Anderson4D.R324WithinHalfResidualPrefix.eventually_integrable_weightedIncomingPhasedHeadLocal_of_integrable {ρ : 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) (postCoefficient : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (postCoefficient ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : ∀ᵐ (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure, MeasureTheory.Integrable (fun (t : Fin (2 * residualBlockOrder head.2) → T4) => ↑((res.headContext head tail hremaining).rawLocalIntegrand ρ ε (res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v) t) * (postCoefficient v * charT4 k ((res.afterHead head tail hremaining).incomingPhaseAnchor x y v) * ↑(res.incomingErasedHeadOuterFactor head tail hremaining ρ ε x y v))) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure)

Full integrability of a phased erased density with a genuinely post-coordinate-dependent coefficient supplies the exact weighted local sections almost everywhere.

The complete local weight is retained. In particular, this statement does not divide by the coefficient or pull an a.e. unweighted statement back through the predecessor-minus-successor map.

One ordinary head

theorem Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_incomingPhasedResidualDensity_eq_afterHead_of_ne_zero {ρ : 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) (postCoefficient : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (postCoefficient ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (w : res.SurvivingCoordinate → T4), res.incomingPhasedResidualDensity (postCoefficient ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2) k ρ ε x y w ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * (res.afterHead head tail hremaining).remainingOrder) * ∫ (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4), (res.afterHead head tail hremaining).incomingPhasedResidualDensity (postCoefficient v) k ρ ε x y v ∂MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure

A head whose predecessor is not slot zero transports the incoming Fourier character and the slot-zero-erased residual core exactly to the post-head phased density.

The coefficient may depend on every surviving post-head coordinate. This is essential for the actual exceptional root, whose untouched outer primitive product is not constant on the residual suffix.