Integral seam after the exceptional incoming head

The exceptional-stop endpoint produces the perturbatively weighted stop Fourier integral over the measured parameter, the retained head tuple, and the after-head surviving tuple. This file integrates the retained head tuple out and identifies the result as exactly the after-head phased residual density consumed by the ordinary-head iteration.

The pointwise head collapse is the genuine-stop anchor decomposition: the head block contributes the squared paper second-order decay, the primitive Step-4 defect, and the transported character at the after-head phase anchor. The decay, the defect, and the untouched post outer factor are absorbed into a genuinely coordinate-dependent post coefficient, while the anchor character and the slot-zero-erased after-head core reassemble the phased density itself. The integrability handover for that density closes the recursion seam.

Pulling the retained head tuple in front of the parameters

def Anderson4D.r324IncomingExceptionalHeadPullMeasurableEquiv (A : Type u_1) (B : Type u_2) (C : Type u_3) [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C] : A × B × C ≃ᵐ B × A × C

Reorder (ω, (t, v)) to (t, (ω, v)), so that the retained head tuple can be integrated first while the measured parameter and the after-head tuple stay joint.

Equations

• Anderson4D.r324IncomingExceptionalHeadPullMeasurableEquiv A B C = MeasurableEquiv.prodComm.trans (MeasurableEquiv.prodAssoc.trans ((MeasurableEquiv.refl B).prodCongr MeasurableEquiv.prodComm))

@[simp]

theorem Anderson4D.r324IncomingExceptionalHeadPullMeasurableEquiv_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C] (a : A) (b : B) (c : C) : (r324IncomingExceptionalHeadPullMeasurableEquiv A B C) (a, b, c) = (b, a, c)

theorem Anderson4D.measurePreserving_r324IncomingExceptionalHeadPullMeasurableEquiv {A : Type u_1} {B : Type u_2} {C : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C] (μA : MeasureTheory.Measure A) (μB : MeasureTheory.Measure B) (μC : MeasureTheory.Measure C) [MeasureTheory.SFinite μA] [MeasureTheory.SFinite μB] [MeasureTheory.SFinite μC] : MeasureTheory.MeasurePreserving (⇑(r324IncomingExceptionalHeadPullMeasurableEquiv A B C)) (μA.prod (μB.prod μC)) (μB.prod (μA.prod μC))

The head pull preserves the corresponding triple product measures.

The erased post-head core at a slot-zero head

theorem Anderson4D.R324WithinHalfResidualPrefix.afterHead_incomingErasedResidualIntegrand_of_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) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : (res.afterHead head tail hremaining).incomingErasedResidualIntegrand ρ' ε' x y ((res.afterHead head tail hremaining).reconstruct v) = res.headOuterFactor head tail hremaining ρ' ε' x y v

At a slot-zero-fed head the erased slot is one of the consumed local slots, so the slot-zero-erased post-head core carries no leftover predecessor factor: it is exactly the ordinary head outer factor.

The after-head phased density produced by the head collapse

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalPostCoefficient {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (k : Z4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (ω : Ω) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) : ℂ

The genuinely coordinate-dependent coefficient left on the after-head phased density once the retained exceptional head has been integrated out: the squared paper second-order decay, the primitive Step-4 defect of the head internal edges, and the untouched post outer factor.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalAfterHeadPhasedIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (p : Ω × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)) : ℂ

The after-head phased residual density carrying the collapsed head as its coordinate-dependent coefficient. This is exactly the incoming phased density form consumed by the ordinary one-head transport equation, at the Fourier-evaluated incoming endpoint 0.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_integral_incomingExceptionalStopFourierDensity_head_eq_afterHeadPhased {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (ω : Ω) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) (hhead : MeasureTheory.Integrable (fun (t : Fin (2 * residualBlockOrder data.terminal.2) → T4) => data.incomingExceptionalStopFourierDensity k y postOuter (ω, t, v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure)) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * residualBlockOrder data.terminal.2) * ∫ (t : Fin (2 * residualBlockOrder data.terminal.2) → T4), data.incomingExceptionalStopFourierDensity k y postOuter (ω, t, v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure) = data.incomingExceptionalAfterHeadPhasedIntegrand k y postOuter (ω, v)

Fixed parameter and after-head coordinates: integrating the retained head tuple produces exactly the after-head phased residual density with the collapsed-head post coefficient.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_incomingExceptionalStopFourierDensity_headPull {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) [MeasureTheory.SFinite ν] (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (hm : 0 < m) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (hsource : MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity k y postOuter) ((paperMeasure.prod ν).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))) : MeasureTheory.Integrable (fun (q : (Fin (2 * residualBlockOrder data.terminal.2) → T4) × Ω × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)) => data.incomingExceptionalStopFourierDensity k y postOuter (q.2.1, q.1, q.2.2)) ((MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure).prod (ν.prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure)))

Joint integrability of the stop Fourier density with the retained head tuple pulled in front of the measured parameter and after-head tuple.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_incomingExceptionalAfterHeadPhasedIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) [MeasureTheory.SFinite ν] (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (hm : 0 < m) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (hsource : MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity k y postOuter) ((paperMeasure.prod ν).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) : MeasureTheory.Integrable (data.incomingExceptionalAfterHeadPhasedIntegrand k y postOuter) (ν.prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure))

Integrability handover. The after-head phased density with the collapsed-head coordinate-dependent coefficient is jointly integrable in the measured parameter and the after-head coordinates. This is the recursion seam feeding the ordinary one-head transport iteration.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_integral_incomingExceptionalStopFourierDensity_eq_afterHead {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) [MeasureTheory.SFinite ν] (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) (hm : 0 < m) (k : Z4) (y : Ω → T4) (postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (hsource : MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity k y postOuter) ((paperMeasure.prod ν).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) : ↑(lamEps lam ε) ^ (2 * data.trace.stopPrefix.remainingOrder) * ∫ (q : Ω × (Fin (2 * residualBlockOrder data.terminal.2) → T4) × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)), data.incomingExceptionalStopFourierDensity k y postOuter q ∂ν.prod ((MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure)) = ↑(lamEps lam ε) ^ (2 * (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).remainingOrder) * ∫ (p : Ω × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)), data.incomingExceptionalAfterHeadPhasedIntegrand k y postOuter p ∂ν.prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure)

Exceptional head absorption at the integral level. The weighted stop Fourier integral collapses its retained head tuple: the perturbative power drops by twice the head block order and the integrand becomes exactly the after-head phased residual density with the collapsed-head coordinate-dependent coefficient.

The genuine refined root

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_incomingExceptionalRefinedRootStopSource {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) : MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity α (fun (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst) => ω.1.1) (data.incomingExceptionalRefinedRootPostOuter α β e₀.snd.snd)) ((paperMeasure.prod (r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst)).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))

The already-proved refined-root joint integrability, transported by the certified trace to the exceptional stop. This is the exact hsource premise of the stop Fubini exchange and of the head absorption.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_r324RefinedPhysicalIntegral_eq_incomingExceptionalAfterHead {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (α β : Z4) : ↑(lamEps lam ε) ^ (2 * (initial ρ lam ε e₀.fst).remainingOrder) * r324RefinedPhysicalIntegral ρ ε m α β p = ↑(lamEps lam ε) ^ (2 * (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).remainingOrder) * ∫ (q : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)), data.incomingExceptionalAfterHeadPhasedIntegrand α (fun (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst) => ω.1.1) (data.incomingExceptionalRefinedRootPostOuter α β e₀.snd.snd) q ∂(r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst).prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure)

Seam-2 endpoint. The genuine single-fibre physical root integral with the retained exceptional head fully absorbed: the right-hand side is the after-head phased density integral over the root parameter and the after-head coordinates, ready for the ordinary-head iteration.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_incomingExceptionalRefinedRootAfterHeadPhasedIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {C K : ℝ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (α β : Z4) : MeasureTheory.Integrable (data.incomingExceptionalAfterHeadPhasedIntegrand α (fun (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst) => ω.1.1) (data.incomingExceptionalRefinedRootPostOuter α β e₀.snd.snd)) ((r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst).prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure))

Integrability handover for the genuine refined root: the seam-2 right-hand density is integrable over the root parameter and the after-head coordinates.