Phased trace: iterating the ordinary transport along the whole suffix

The one-head ordinary transport and its integrability seam advance the incoming phased residual density across one non-slot-zero-fed head. This file iterates that step along a complete certified analytic trace, from an arbitrary residual prefix down to the terminal prefix with empty remaining list, and composes the result with the exceptional-head base case at the genuine refined physical root.

The certified analytic trace already stores the per-head internal Fubini evidence and edge certificates. The single genuinely new hypothesis is OrdinaryAlong: every head traversed by the trace must have a nonzero sparse predecessor slot, so that the slot-zero-erased phase representation is preserved. This is not derivable from the stop certificate: a schedule may contain a later block all of whose earlier vertices have already been consumed, and such a block is fed by slot zero. The hypothesis is therefore taken pointwise along the trace and must be discharged by the caller from the combinatorics of the concrete schedule.

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.OrdinaryAlong {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) : Prop

Every head traversed by a certified analytic trace has a nonzero sparse predecessor slot. This is exactly the hypothesis under which the ordinary phased one-head transport applies at every step.

Equations

• One or more equations did not get rendered due to their size.
• (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminal res scale hremaining certificate).OrdinaryAlong = True

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.ordinaryAlong_of_predecessorSlot_ne_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) (hpreds : ∀ (res' : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)), res'.remaining = head :: tail → res'.remaining <:+ res.remaining → r324WithinHalfPredecessorSlot res'.state head ≠ 0) : trace.OrdinaryAlong

Ordinariness along a certified analytic trace follows from the purely combinatorial statement that every prefix whose remaining list is a suffix of the starting remaining list has a nonzero sparse predecessor slot at its head. The predecessor slot depends only on the processed schedule prefix, so this hypothesis is a property of the schedule decomposition alone, independent of the trace.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.integrable_trace_end_incomingPhasedResidualDensity {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (x y : T4) (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) (hordinary : trace.OrdinaryAlong) (coefficient : (trace.terminalPrefix.SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (coefficient (trace.terminalProjection w)) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : MeasureTheory.Integrable (fun (v : trace.terminalPrefix.SurvivingCoordinate → T4) => trace.terminalPrefix.incomingPhasedResidualDensity (coefficient v) k ρ ε x y v) (MeasureTheory.Measure.pi fun (x : trace.terminalPrefix.SurvivingCoordinate) => paperMeasure)

Terminal integrability along an ordinary phased trace. Full integrability of the phased density at the root of the trace transports to the terminal prefix, with the coefficient read through the terminal projection at every intermediate step.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.lamEps_pow_integral_incomingPhasedResidualDensity_eq_trace_end {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (x y : T4) (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) (hordinary : trace.OrdinaryAlong) (coefficient : (trace.terminalPrefix.SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (coefficient (trace.terminalProjection w)) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (w : res.SurvivingCoordinate → T4), res.incomingPhasedResidualDensity (coefficient (trace.terminalProjection w)) k ρ ε x y w ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * trace.terminalPrefix.remainingOrder) * ∫ (v : trace.terminalPrefix.SurvivingCoordinate → T4), trace.terminalPrefix.incomingPhasedResidualDensity (coefficient v) k ρ ε x y v ∂MeasureTheory.Measure.pi fun (x : trace.terminalPrefix.SurvivingCoordinate) => paperMeasure

Phased trace recursion. Along a certified analytic trace all of whose heads are ordinary, the weighted incoming phased residual integral transports exactly to the terminal prefix: the perturbative power drops to twice the terminal remaining order and the density becomes the terminal phased density with the same coefficient, phase, and endpoints.

The certified analytic trace of the after-head suffix

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.afterHeadCertifiedAnalyticTrace {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κp : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κp) : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfCertifiedAnalyticTrace (r324WithinHalfUpdatedEdgeScale data.stopContext data.stopScale C lam K)

The certified analytic trace of the complete after-head suffix, built from the local block provider and the certificate transported to the exceptional stop. Only the ordinariness of the suffix heads is not provided by this construction.

Equations

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

The genuine root coefficient at the terminal carrier

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalRefinedRootTerminalPostOuter {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) {scale : Fin (m + 1) → ℝ} (trace : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfCertifiedAnalyticTrace scale) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) (ω : R324IncomingExceptionalRootParameter ρ lam ε κm) (u : trace.terminalPrefix.SurvivingCoordinate → T4) : ℂ

The untouched refined-root outer functional read on the terminal carrier of a certified after-head trace: the retained endpoint characters, the untouched right initial residual, and the cross-cut primitive factor reconstructed from the terminal prefix.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalRefinedRootPostOuter_eq_terminalProjection {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) {scale : Fin (m + 1) → ℝ} (trace : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfCertifiedAnalyticTrace scale) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) (ω : R324IncomingExceptionalRootParameter ρ lam ε κm) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) : data.incomingExceptionalRefinedRootPostOuter α β π ω v = data.incomingExceptionalRefinedRootTerminalPostOuter trace α β π ω (trace.terminalProjection v)

Terminal factorization of the refined-root outer functional. The cross-cut primitive factor reads only coordinates on the doubled residual carrier, all of which survive to the terminal prefix; hence the whole refined-root outer functional factors through the terminal projection of any certified after-head trace.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalRefinedRootTerminalCoefficient {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) {scale : Fin (m + 1) → ℝ} (trace : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfCertifiedAnalyticTrace scale) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) (ω : R324IncomingExceptionalRootParameter ρ lam ε κm) (u : trace.terminalPrefix.SurvivingCoordinate → T4) : ℂ

The collapsed-head coefficient of the genuine refined root, read on the terminal carrier: squared second-order decay, primitive Step-4 defect of the exceptional head, and the terminal form of the untouched refined outer functional.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalPostCoefficient_refinedRoot_eq_terminalProjection {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) {scale : Fin (m + 1) → ℝ} (trace : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfCertifiedAnalyticTrace scale) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) (ω : R324IncomingExceptionalRootParameter ρ lam ε κm) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) : data.incomingExceptionalPostCoefficient α (data.incomingExceptionalRefinedRootPostOuter α β π) ω v = data.incomingExceptionalRefinedRootTerminalCoefficient trace α β π ω (trace.terminalProjection v)

The collapsed-head refined-root coefficient factors through the terminal projection of any certified after-head trace.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalAfterHeadPhasedIntegrand_refinedRoot_section_eq {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κp κm : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) {scale : Fin (m + 1) → ℝ} (trace : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfCertifiedAnalyticTrace scale) (α β : Z4) (π : ↥κp.singles ≃ ↥κm.singles) (ω : R324IncomingExceptionalRootParameter ρ lam ε κm) : (fun (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => data.incomingExceptionalAfterHeadPhasedIntegrand α (fun (ω' : R324IncomingExceptionalRootParameter ρ lam ε κm) => ω'.1.1) (data.incomingExceptionalRefinedRootPostOuter α β π) (ω, v)) = fun (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).incomingPhasedResidualDensity (data.incomingExceptionalRefinedRootTerminalCoefficient trace α β π ω (trace.terminalProjection v)) α ρ ε 0 ω.1.1 v

At a fixed root parameter, the after-head phased integrand of the genuine refined root is the after-head phased density whose coefficient is the terminal refined coefficient read through the terminal projection.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_r324RefinedPhysicalIntegral_eq_incomingExceptionalTraceEnd {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) {scale : Fin (m + 1) → ℝ} (trace : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfCertifiedAnalyticTrace scale) (hordinary : trace.OrdinaryAlong) (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 * trace.terminalPrefix.remainingOrder) * ∫ (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst), ∫ (u : trace.terminalPrefix.SurvivingCoordinate → T4), trace.terminalPrefix.incomingPhasedResidualDensity (data.incomingExceptionalRefinedRootTerminalCoefficient trace α β e₀.snd.snd ω u) α ρ ε 0 ω.1.1 u ∂MeasureTheory.Measure.pi fun (x : trace.terminalPrefix.SurvivingCoordinate) => paperMeasure ∂r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst

Full phased trace of the genuine refined root. The weighted single-fibre refined physical integral, with the exceptional head absorbed by the base case and every later suffix head absorbed by the ordinary phased iteration: the right-hand side integrates the terminal phased density over the root parameter and the terminal coordinates, with the collapsed-head refined coefficient read on the terminal carrier.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eventually_integrable_incomingExceptionalRefinedRootTraceEnd {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) {scale : Fin (m + 1) → ℝ} (trace : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfCertifiedAnalyticTrace scale) (hordinary : trace.OrdinaryAlong) (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) : ∀ᵐ (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst) ∂r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst, MeasureTheory.Integrable (fun (u : trace.terminalPrefix.SurvivingCoordinate → T4) => trace.terminalPrefix.incomingPhasedResidualDensity (data.incomingExceptionalRefinedRootTerminalCoefficient trace α β e₀.snd.snd ω u) α ρ ε 0 ω.1.1 u) (MeasureTheory.Measure.pi fun (x : trace.terminalPrefix.SurvivingCoordinate) => paperMeasure)

Terminal integrability at the genuine refined root. For almost every root parameter, the terminal phased density with the refined terminal coefficient is integrable over the terminal coordinates. This is the endpoint form of the trace integrability seam, ready for the final incoming Fourier evaluation and the branch summation.