Root joint integrability at an exceptional incoming stop

This module reindexes one genuine residual-refined physical fibre so that the left initial residual is the last coordinate, while the remaining endpoints and the right initial residual form the measured parameter of the incoming-stop trace. The already proved root integrability then supplies the trace/Fourier bridge directly.

@[reducible, inline]

abbrev Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalRootParameter (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κm : PartialPairing (Fin m)) : Type

The three endpoints not integrated at the incoming stop, together with the untouched right initial residual tuple.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324IncomingExceptionalRootParameterMeasure (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κm : PartialPairing (Fin m)) : MeasureTheory.Measure (R324IncomingExceptionalRootParameter ρ lam ε κm)

Product Haar measure on the incoming-stop root parameter.

Equations

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

instance Anderson4D.R324WithinHalfResidualPrefix.instSFiniteR324IncomingExceptionalRootParameterMeasure (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κm : PartialPairing (Fin m)) : MeasureTheory.SFinite (r324IncomingExceptionalRootParameterMeasure ρ lam ε κm)

@[reducible, inline]

abbrev Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalRootPoint (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) : Type

Root coordinates in the order expected by the exceptional-stop trace: the incoming endpoint and measured parameter first, then the left initial residual tuple.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.r324IncomingExceptionalRootMeasurableEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) : R324PhysicalPoint m ≃ᵐ R324IncomingExceptionalRootPoint ρ lam ε κp κm

Reindex (x,y,z,w,v) as ((x,((y,z,w),vr)),vl), where the doubled tuple v is split into the two literal initial sparse carriers.

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.r324IncomingExceptionalRootMeasurableEquiv_apply (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) (q : R324PhysicalPoint m) : (r324IncomingExceptionalRootMeasurableEquiv ρ lam ε κp κm) q = ((q.1, (q.2.1, q.2.2.1, q.2.2.2.1), ((r324InitialTwoHalfProductPiMeasurableEquiv ρ lam ε κp κm).symm q.2.2.2.2).2), ((r324InitialTwoHalfProductPiMeasurableEquiv ρ lam ε κp κm).symm q.2.2.2.2).1)

theorem Anderson4D.R324WithinHalfResidualPrefix.measurePreserving_r324IncomingExceptionalRootMeasurableEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) : MeasureTheory.MeasurePreserving (⇑(r324IncomingExceptionalRootMeasurableEquiv ρ lam ε κp κm)) (r324PhysicalMeasure m) ((paperMeasure.prod (r324IncomingExceptionalRootParameterMeasure ρ lam ε κm)).prod (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε κp).SurvivingCoordinate) => paperMeasure))

The root reindexing preserves the exact product Haar measures.

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

Remaining endpoint characters, the untouched right residual density, and the cross-cut factor read after the retained left head.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324Flatten_momentRefinedPhysicalIntegrand_eq_initialSource_reindex {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} (e₀ : MomentContraction m) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (he₀ : e₀ ∈ momentRefinedContractionFiber m s r) (q : R324PhysicalPoint m) : r324Flatten (momentRefinedPhysicalIntegrand ρ ε m α β s r) q = data.incomingExceptionalInitialSourceDensity α (fun (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst) => ω.1.1) (data.incomingExceptionalRefinedRootPostOuter α β e₀.snd.snd) ((r324IncomingExceptionalRootMeasurableEquiv ρ lam ε e₀.fst e₀.snd.fst) q)

Under the exact root reindexing, the genuine refined physical density is the initial source density consumed by the exceptional-stop trace.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_incomingExceptionalRefinedInitialSource {ρ : 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) (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) : MeasureTheory.Integrable (data.incomingExceptionalInitialSourceDensity α (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 : (initial ρ lam ε e₀.fst).SurvivingCoordinate) => paperMeasure))

The genuine refined-root integrability theorem supplies exactly the single hcurrent premise consumed by the exceptional trace/Fourier bridge.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_integral_refinedInitialSource_eq_incomingExceptionalStopFourier {ρ : 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) (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) : ↑(lamEps lam ε) ^ (2 * (initial ρ lam ε e₀.fst).remainingOrder) * ∫ (q : (T4 × R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst) × ((initial ρ lam ε e₀.fst).SurvivingCoordinate → T4)), data.incomingExceptionalInitialSourceDensity α (fun (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst) => ω.1.1) (data.incomingExceptionalRefinedRootPostOuter α β e₀.snd.snd) q ∂(paperMeasure.prod (r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst)).prod (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε e₀.fst).SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * data.trace.stopPrefix.remainingOrder) * ∫ (q : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst × (Fin (2 * residualBlockOrder data.terminal.2) → T4) × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)), data.incomingExceptionalStopFourierDensity α (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 : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure))

Root integrability is discharged internally before the certified left trace and incoming-endpoint Fourier evaluation are composed. Callers supply only the realized refined representative and its fibre membership; there is no residual hcurrent or Fubini premise.