From the initial R-324 trace to an incoming stop Fourier density

This module composes two exact operations:

• certified integration of every analytic block before an exceptional incoming stop; and
• endpoint-first Fourier evaluation at that stop.

The retained exceptional head and its complete suffix remain uncollapsed. Consequently the right-hand side keeps the exact perturbative power of the whole stopping suffix.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalInitialSourceDensity {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : 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 : (T4 × Ω) × ((initial ρ lam ε κ).SurvivingCoordinate → T4)) : ℂ

The genuine density at the all-Green initial prefix whose incoming endpoint will be Fourier transformed at the certified exceptional stop.

The character precedes the post-stop outer factor, exactly as in incomingExceptionalStopSourceDensity.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_integral_initialResidual_eq_incomingExceptionalStopFourier {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : 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) → ℂ) (hcurrent : MeasureTheory.Integrable (data.incomingExceptionalInitialSourceDensity k y postOuter) ((paperMeasure.prod ν).prod (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κ).SurvivingCoordinate) => paperMeasure))) : ↑(lamEps lam ε) ^ (2 * (initial ρ lam ε κ).remainingOrder) * ∫ (p : (T4 × Ω) × ((initial ρ lam ε κ).SurvivingCoordinate → T4)), data.incomingExceptionalInitialSourceDensity k y postOuter p ∂(paperMeasure.prod ν).prod (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κ).SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * data.trace.stopPrefix.remainingOrder) * ∫ (p : Ω × (Fin (2 * residualBlockOrder data.terminal.2) → T4) × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)), data.incomingExceptionalStopFourierDensity k y postOuter p ∂ν.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))

Exact transport from the all-Green initial residual integral to the incoming-endpoint Fourier density at an exceptional stop.

One genuine initial joint-integrability premise licenses both the complete prefix trace and the endpoint Fubini exchange. No additional stop integrability or weighted-trace premise is assumed.