Physical refined roots at an exceptional incoming stop #
This module closes the exact product-space reindex between one literal
residual-refined physical fibre and the initial source density consumed by
an exceptional incoming trace. It then exposes the existing trace/Fourier
identity with r324RefinedPhysicalIntegral itself on the left.
No sum over refined schedule fibres is performed here.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324RefinedPhysicalIntegral_eq_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)
(α β : Z4)
:
r324RefinedPhysicalIntegral ρ ε m α β p = ∫ (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)
The literal physical integral of one refined schedule fibre is exactly the reindexed initial source integral used by an exceptional incoming left trace.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_r324RefinedPhysicalIntegral_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) * r324RefinedPhysicalIntegral ρ ε m α β p = ↑(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))
The exceptional incoming trace/Fourier identity with the genuine single-fibre physical root integral on the left. Root integrability and all Fubini premises are discharged internally.