Exact iteration of the R-322 residual invariant #
Paper: R-322 — §4.1 → (3.22): the constructive renormalization-constant bound
This module iterates the one-proper-block identity proved in
R322AnalyticResidualPrefixInvariant and identifies the final singleton
whole-carrier residual with the terminal heterogeneous primitive integral.
theorem
Anderson4D.R322AnalyticTerminalStepContext.blockOrderIso_zero
{q : ℕ}
{hq : 1 ≤ q}
(ctx : R322AnalyticTerminalStepContext q hq)
:
The first point in the increasing terminal carrier is the global left endpoint.
theorem
Anderson4D.R322AnalyticTerminalStepContext.successorVertex_internalEdge
{q : ℕ}
{hq : 1 ≤ q}
(ctx : R322AnalyticTerminalStepContext q hq)
(j : Fin (2 * residualBlockOrder ctx.terminal.2 - 1))
:
r322AnalyticSuccessorVertex ctx.state (r322AnalyticEdgeLeftVertex (ctx.internalEdge j)) ⋯ = ↑(ctx.blockOrderIso ⟨↑j + 1, ⋯⟩)
The sparse successor of a terminal-chain left vertex is its next vertex in the increasing terminal block enumeration.
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_remainingOrder
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
:
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_one_le_blockOrder
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
:
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_remainingRightValues
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
:
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_residualStepDifference
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(x : Fin (2 * q) → T4)
:
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_residualDifferenceProduct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(x : Fin (2 * q) → T4)
:
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_remainingBlockIndex_zero
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
:
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_residualPrimitiveProduct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(ρ' : SmoothCutoff)
(ε' : ℝ)
(x : Fin (2 * q) → T4)
:
res.residualPrimitiveProduct ρ' ε' x = r322ExtractionBlockPrimitiveSum ρ' ε' res.pairing (res.remainingBlockIndex ⟨0, ⋯⟩) x
def
Anderson4D.R322AnalyticResidualPrefix.terminalBlockOrderIso
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res' : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal' : R322ExtractionStep (2 * q))
(hremaining' : res'.remaining = [terminal'])
(hterminal' : terminal'.1 = r322WholeEndpoint q hq)
:
Stable terminal-block order whose source mentions the displayed terminal step rather than the reducible context field.
Equations
- res'.terminalBlockOrderIso terminal' hremaining' hterminal' = Anderson4D.residualPrimitiveBlockOrderIso res'.pairing terminal'.2 ⋯
Instances For
theorem
Anderson4D.R322AnalyticResidualPrefix.terminalBlockOrderIso_apply_eq_context
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(i : Fin (2 * residualBlockOrder terminal.2))
:
↑((res.terminalBlockOrderIso terminal hremaining hterminal) i) = ↑((Anderson4D.R322AnalyticResidualPrefix.terminalContext✝ res terminal hremaining hterminal).blockOrderIso i)
theorem
Anderson4D.R322AnalyticResidualPrefix.terminalBlockOrderIso_zero
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
:
theorem
Anderson4D.R322AnalyticResidualPrefix.terminalBlockOrderIso_last
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
:
↑((res.terminalBlockOrderIso terminal hremaining hterminal) (primitiveLast (residualBlockOrder terminal.2) ⋯)) = ⟨2 * q - 1, ⋯⟩
def
Anderson4D.R322AnalyticResidualPrefix.terminalBlockTuple
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res' : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal' : R322ExtractionStep (2 * q))
(hremaining' : res'.remaining = [terminal'])
(hterminal' : terminal'.1 = r322WholeEndpoint q hq)
(x : Fin (2 * q) → T4)
:
Fin (2 * residualBlockOrder terminal'.2) → T4
The ambient tuple read in the increasing order of the terminal active carrier.
Equations
- res'.terminalBlockTuple terminal' hremaining' hterminal' x i = x ↑((res'.terminalBlockOrderIso terminal' hremaining' hterminal') i)
Instances For
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_residualChainEdgeFactor_internal
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(x : Fin (2 * q) → T4)
(j : Fin (2 * residualBlockOrder terminal.2 - 1))
:
res.residualChainEdgeFactor x
((Anderson4D.R322AnalyticResidualPrefix.terminalContext✝ res terminal hremaining hterminal).internalEdge j) = (Anderson4D.R322AnalyticResidualPrefix.terminalContext✝ res terminal hremaining hterminal).internalEdges j
(res.terminalBlockTuple terminal hremaining hterminal x ⟨↑j, ⋯⟩ - res.terminalBlockTuple terminal hremaining hterminal x ⟨↑j + 1, ⋯⟩)
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_residualChainEdgeFactor_eq_one_of_not_active
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(x : Fin (2 * q) → T4)
(edge : Fin (2 * q - 1))
(hedge : edge ∉ r322AnalyticActiveEdges res.state)
:
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_residualChainProduct
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(x : Fin (2 * q) → T4)
:
res.residualChainProduct x = primitiveChainProduct (residualBlockOrder terminal.2) ⋯
(Anderson4D.R322AnalyticResidualPrefix.terminalContext✝ res terminal hremaining hterminal).internalEdges
(res.terminalBlockTuple terminal hremaining hterminal x)
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_residualPrimitiveProduct_eq_covarianceSum
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(ρ' : SmoothCutoff)
(ε' : ℝ)
(x : Fin (2 * q) → T4)
:
res.residualPrimitiveProduct ρ' ε' x = ∑ κB : ↥(primitiveFullPairings (residualBlockOrder terminal.2)),
primitiveCovarianceProduct ρ' ε' (residualBlockOrder terminal.2) (↑κB)
(res.terminalBlockTuple terminal hremaining hterminal x)
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_residualIntegrand_eq_closedSum
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(ρ' : SmoothCutoff)
(ε' : ℝ)
(x : Fin (2 * q) → T4)
:
res.residualIntegrand ρ' ε' x = ∑ κB : ↥(primitiveFullPairings (residualBlockOrder terminal.2)),
detJclosedIntegrandWith ρ' ε' (2 * residualBlockOrder terminal.2) (↑κB)
(Anderson4D.R322AnalyticResidualPrefix.terminalContext✝ res terminal hremaining hterminal).internalEdges
(res.terminalBlockTuple terminal hremaining hterminal x)
def
Anderson4D.R322AnalyticResidualPrefix.terminalInternalCoordinateEquiv
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
:
Increasing internal terminal-block positions are exactly the surviving spatial coordinates of a singleton whole-carrier residual.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Anderson4D.R322AnalyticResidualPrefix.terminalInternalPiMeasurableEquiv
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
:
Product-coordinate reindex from the terminal residual carrier to the standard internal primitive coordinates.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R322AnalyticResidualPrefix.measurePreserving_terminalInternalPiMeasurableEquiv
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
:
MeasureTheory.MeasurePreserving (⇑(res.terminalInternalPiMeasurableEquiv terminal hremaining hterminal))
(MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder terminal.2 - 2)) => paperMeasure)
@[simp]
theorem
Anderson4D.R322AnalyticResidualPrefix.terminalInternalPiMeasurableEquiv_apply
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(v : res.SurvivingCoordinate → T4)
(j : Fin (2 * residualBlockOrder terminal.2 - 2))
:
(res.terminalInternalPiMeasurableEquiv terminal hremaining hterminal) v j = v ((res.terminalInternalCoordinateEquiv terminal hremaining hterminal) j)
theorem
Anderson4D.R322AnalyticResidualPrefix.terminalBlockTuple_reconstruct_eq_primitiveAssemble
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(z : T4)
(v : res.SurvivingCoordinate → T4)
:
res.terminalBlockTuple terminal hremaining hterminal (res.reconstruct z v) = primitiveAssemble (residualBlockOrder terminal.2) ⋯ z 0
((res.terminalInternalPiMeasurableEquiv terminal hremaining hterminal) v)
theorem
Anderson4D.R322AnalyticResidualPrefix.terminal_residualValue_eq_terminalSpatialIntegral
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : res.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(z : T4)
:
res.residualValue ρ lam ε z = (Anderson4D.R322AnalyticResidualPrefix.terminalContext✝ res terminal hremaining hterminal).terminalSpatialIntegral ρ
lam ε z 0
A singleton whole-carrier residual is exactly the terminal heterogeneous primitive integral, with no division by the coupling and no nonzero-power side condition.
theorem
Anderson4D.R322AnalyticResidualPrefix.eventually_integrable_weightedLocal_of_integrable
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(step : R322ExtractionStep (2 * q))
(suffix : List (R322ExtractionStep (2 * q)))
(hremaining : res.remaining = step :: suffix)
(hproper : step.1 ≠ r322WholeEndpoint q hq)
(z : T4)
(hint :
MeasureTheory.Integrable (fun (v : res.SurvivingCoordinate → T4) => res.residualIntegrand ρ ε (res.reconstruct z v))
(MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))
:
let ctx := res.properStepContext step suffix hremaining hproper;
have post := res.afterProper step suffix hremaining hproper;
have base := fun (outer : post.SurvivingCoordinate → T4) => post.reconstruct z outer;
have outerFactor := fun (outer : post.SurvivingCoordinate → T4) =>
res.properOuterIntegrand step suffix hremaining hproper ρ ε (base outer);
∀ᵐ (outer : post.SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : post.SurvivingCoordinate) => paperMeasure, MeasureTheory.Integrable
(fun (t : Fin (2 * residualBlockOrder step.2) → T4) =>
ctx.rawLocalIntegrand ρ ε (ctx.predecessorPoint (base outer) - ctx.successorPoint (base outer)) t * outerFactor outer)
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder step.2)) => paperMeasure)
Full current-residual integrability gives the exact weighted local section integrability needed at almost every genuine outer coordinate. The weight is retained: no invalid cancellation is made on its zero set.
theorem
Anderson4D.R322AnalyticResidualPrefix.R322AnalyticProperStepContext.rawLocalSpatialIntegral_mul_outer_eq_nextState_of_weighted
{q : ℕ}
{hq : 1 ≤ q}
(ctx : R322AnalyticProperStepContext q hq)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(u : T4)
(outer : ℝ)
(hweighted :
MeasureTheory.Integrable
(fun (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) => ctx.rawLocalIntegrand ρ ε u t * outer)
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure))
(hinternal :
∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))),
MeasureTheory.Integrable
(fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges
(primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure))
:
(lamEps lam ε ^ (2 * residualBlockOrder ctx.step.2) * ∫ (t : Fin (2 * residualBlockOrder ctx.step.2) → T4), ctx.rawLocalIntegrand ρ ε u t * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure) = (ctx.nextState ρ lam ε).edges ctx.predecessorEdge u * outer
A weighted local section suffices for the exact collapse. On the zero weight set both sides vanish; away from it, scalar cancellation recovers the unweighted local integrability required by the existing Fubini theorem.
theorem
Anderson4D.R322AnalyticResidualPrefix.R322AnalyticProperStepContext.processedResidualOuterIntegral_eq_updated_of_weighted
{q : ℕ}
{hq : 1 ≤ q}
(ctx : R322AnalyticProperStepContext q hq)
{Ω : Type u_1}
[MeasurableSpace Ω]
(ν : MeasureTheory.Measure Ω)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(base : Ω → Fin (2 * q) → T4)
(outer : Ω → ℝ)
(hweighted :
∀ᵐ (ω : Ω) ∂ν, MeasureTheory.Integrable
(fun (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) =>
ctx.rawLocalIntegrand ρ ε (ctx.predecessorPoint (base ω) - ctx.successorPoint (base ω)) t * outer ω)
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure))
(hinternal :
∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))),
MeasureTheory.Integrable
(fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges
(primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure))
:
ctx.processedResidualOuterIntegral ν ρ lam ε base outer = ctx.updatedResidualOuterIntegral ν ρ lam ε base outer
Weighted-section form of the exact outer substitution.
theorem
Anderson4D.R322AnalyticResidualPrefix.residualValue_eq_afterProper_of_integrable
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(step : R322ExtractionStep (2 * q))
(suffix : List (R322ExtractionStep (2 * q)))
(hremaining : res.remaining = step :: suffix)
(hproper : step.1 ≠ r322WholeEndpoint q hq)
(z : T4)
(hint :
MeasureTheory.Integrable (fun (v : res.SurvivingCoordinate → T4) => res.residualIntegrand ρ ε (res.reconstruct z v))
(MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))
(hinternal :
∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder step.2))),
MeasureTheory.Integrable
(fun (v : Fin (2 * residualBlockOrder step.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder step.2) (↑κB)
(res.properStepContext step suffix hremaining hproper).internalEdges
(primitiveAssemble (residualBlockOrder step.2) ⋯ p.1 p.2 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder step.2 - 2)) => paperMeasure))
:
res.residualValue ρ lam ε z = (res.afterProper step suffix hremaining hproper).residualValue ρ lam ε z
Strengthened exact one-step residual identity. Full current integrability supplies weighted sections automatically, so the only separate Fubini premise is the genuine closed-primitive section integrability.
theorem
Anderson4D.R322AnalyticResidualPrefix.integrable_residualIntegrand_afterProper_of_weighted
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(step : R322ExtractionStep (2 * q))
(suffix : List (R322ExtractionStep (2 * q)))
(hremaining : res.remaining = step :: suffix)
(hproper : step.1 ≠ r322WholeEndpoint q hq)
(z : T4)
(hint :
MeasureTheory.Integrable (fun (v : res.SurvivingCoordinate → T4) => res.residualIntegrand ρ ε (res.reconstruct z v))
(MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))
(hinternal :
∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder step.2))),
MeasureTheory.Integrable
(fun (v : Fin (2 * residualBlockOrder step.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder step.2) (↑κB)
(res.properStepContext step suffix hremaining hproper).internalEdges
(primitiveAssemble (residualBlockOrder step.2) ⋯ p.1 p.2 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder step.2 - 2)) => paperMeasure))
:
MeasureTheory.Integrable
(fun (outer : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate → T4) =>
(res.afterProper step suffix hremaining hproper).residualIntegrand ρ ε
((res.afterProper step suffix hremaining hproper).reconstruct z outer))
(MeasureTheory.Measure.pi fun (x : (res.afterProper step suffix hremaining hproper).SurvivingCoordinate) =>
paperMeasure)
Full residual integrability is preserved by one genuine proper collapse without a separate standard-section hypothesis. The current full integrability supplies exactly the weighted local sections needed by the scalar-safe collapse identity.
structure
Anderson4D.R322AnalyticResidualPrefix.ProperStepPremises
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(res : R322AnalyticResidualPrefix ρ lam ε q hq)
(z : T4)
(step : R322ExtractionStep (2 * q))
(suffix : List (R322ExtractionStep (2 * q)))
(hremaining : res.remaining = step :: suffix)
(hproper : step.1 ≠ r322WholeEndpoint q hq)
:
The exact analytic side conditions consumed by one proper residual transition at the displayed external endpoint.
- internal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder step.2) (↑κB) (res.properStepContext step suffix hremaining hproper).internalEdges (primitiveAssemble (residualBlockOrder step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder step.2 - 2)) => paperMeasure)
Instances For
inductive
Anderson4D.R322AnalyticResidualPrefix.ProperRun
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(z : T4)
:
R322AnalyticResidualPrefix ρ lam ε q hq → R322AnalyticResidualPrefix ρ lam ε q hq → Prop
A finite exact proper-prefix run. Every constructor records the actual section-integrability facts used by Fubini; no global assumption or hidden pointwise-to-a.e. pullback is built into the trace.
- refl {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} {z : T4} (res : R322AnalyticResidualPrefix ρ lam ε q hq) : ProperRun z res res
- step {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} {z : T4} (res : R322AnalyticResidualPrefix ρ lam ε q hq) (current : R322ExtractionStep (2 * q)) (suffix : List (R322ExtractionStep (2 * q))) (hremaining : res.remaining = current :: suffix) (hproper : current.1 ≠ r322WholeEndpoint q hq) (premises : res.ProperStepPremises z current suffix hremaining hproper) {finish : R322AnalyticResidualPrefix ρ lam ε q hq} (tail : ProperRun z (res.afterProper current suffix hremaining hproper) finish) : ProperRun z res finish
Instances For
theorem
Anderson4D.R322AnalyticResidualPrefix.ProperRun.residualValue_eq
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
{start finish : R322AnalyticResidualPrefix ρ lam ε q hq}
{z : T4}
(run : ProperRun z start finish)
(hint :
MeasureTheory.Integrable
(fun (v : start.SurvivingCoordinate → T4) => start.residualIntegrand ρ ε (start.reconstruct z v))
(MeasureTheory.Measure.pi fun (x : start.SurvivingCoordinate) => paperMeasure))
:
Exact value invariance and full integrability propagate together along an honest proper run.
structure
Anderson4D.R322AnalyticResidualPrefix.R322AnalyticAlignedTerminalData
{q : ℕ}
(hq : 1 ≤ q)
(ρ : SmoothCutoff)
(C lam ε K A : ℝ)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(z : T4)
:
One terminal object carrying both the exact residual run and the
quantitative edge data used by its final majorant. All fields refer to the
same finish.state; no comparison between separately selected terminal
contexts is needed downstream.
- finish : R322AnalyticResidualPrefix ρ lam ε q hq
- terminal : R322ExtractionStep (2 * q)
- budgetReachable : R322AnalyticBudgetScaleReachable hq ρ C lam ε K A κ hκ self.finish.state self.scale
- edgeCertificate : R322AnalyticEdgeCertificate self.finish.state self.scale
Instances For
theorem
Anderson4D.R322AnalyticResidualPrefix.exists_r322AnalyticAlignedTerminalData
(ρ : SmoothCutoff)
:
∃ (supportConstant : ℝ) (C : ℝ) (K : ℝ) (A : ℝ),
0 < supportConstant ∧ 0 < C ∧ 0 < K ∧ 1 ≤ A ∧ (∀ (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ),
0 < lam →
0 < ε →
ε ≤ 1 →
n ≤ truncOrder ε →
IsAdmissiblePrimitiveInput n G →
MemEClassT4 (primitiveKernelDiff ρ lam ε n hn G) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε n hn G) ∧ PrimitiveKernelBounds ρ lam ε n hn G supportConstant C) ∧ ∀ (lam ε : ℝ) (q : ℕ) (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q)
(z : T4),
0 < lam →
0 < ε →
ε ≤ 1 →
1 ≤ |Real.log ε| →
q ≤ truncOrder ε → Nonempty (R322AnalyticAlignedTerminalData hq ρ C lam ε K A κ hκ z)
The canonical proper prefix admits an honest exact run. Quantitative edge certificates are propagated on the very same residual object, rather than selecting unrelated states with the same processed list.
theorem
Anderson4D.R322AnalyticResidualPrefix.exists_canonical_properRun
(ρ : SmoothCutoff)
(lam ε : ℝ)
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(z : T4)
(hlam : 0 < lam)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(hlog : 1 ≤ |Real.log ε|)
(hqtrunc : q ≤ truncOrder ε)
:
∃ (finish : R322AnalyticResidualPrefix ρ lam ε q hq) (terminal : R322ExtractionStep (2 * q)),
finish.remaining = [terminal] ∧ terminal.1 = r322WholeEndpoint q hq ∧ ProperRun z (initial ρ lam ε hq κ hκ) finish
Run-only projection of the aligned quantitative construction.
theorem
Anderson4D.R322AnalyticResidualPrefix.endpointFiberDetJSum_eq_terminalSpatialIntegral_of_run
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{hq : 1 ≤ q}
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(z : T4)
(finish : R322AnalyticResidualPrefix ρ lam ε q hq)
(terminal : R322ExtractionStep (2 * q))
(hremaining : finish.remaining = [terminal])
(hterminal : terminal.1 = r322WholeEndpoint q hq)
(run : ProperRun z (initial ρ lam ε hq κ hκ) finish)
(hint :
∀ (τ : ReductionEndpointFiberAt κ),
MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure))
:
endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = (Anderson4D.R322AnalyticResidualPrefix.terminalContext✝ finish terminal hremaining hterminal).terminalSpatialIntegral
ρ lam ε z 0
Endpoint-fibre exact identity furnished by any complete honest proper run ending at its singleton whole-carrier residual.
theorem
Anderson4D.R322AnalyticResidualPrefix.integrable_detJintegrand_zeroEndpoint
(ρ : SmoothCutoff)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(q : ℕ)
(hq : 1 ≤ q)
(σ : PartialPairing (Fin (2 * q)))
:
MeasureTheory.Integrable
(fun (p : T4 × (Fin (2 * q - 2) → T4)) => detJintegrand ρ ε q σ (primitiveAssemble q hq p.1 0 p.2))
(paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure))
Joint integrability of one frozen J summand with the terminal
endpoint fixed at zero. This retains the internal variables, unlike
integrable_detJ_zero, and is therefore the genuine source of the
almost-everywhere fixed-endpoint sections used below.
theorem
Anderson4D.R322AnalyticResidualPrefix.eventually_integrable_endpointFiber_sections
(ρ : SmoothCutoff)
{ε : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
:
∀ᵐ (z : T4) ∂paperMeasure, ∀ (τ : ReductionEndpointFiberAt κ),
MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure)
Every summand in one endpoint-signature fibre has an integrable internal section for almost every external endpoint.
theorem
Anderson4D.R322AnalyticResidualPrefix.exists_r322AnalyticAlignedEndpointMajorant
(ρ : SmoothCutoff)
:
∃ (supportConstant : ℝ) (primitiveConstant : ℝ),
0 < supportConstant ∧ 0 < primitiveConstant ∧ ∀ (lam ε : ℝ) (q : ℕ) (hq : 1 ≤ q),
∀ κ ∈ nonSplitPairings q,
∀ (z : T4),
0 < lam →
0 < ε →
ε ≤ 1 →
1 ≤ |Real.log ε| →
q ≤ truncOrder ε →
z ≠ 0 →
(∀ (τ : ReductionEndpointFiberAt κ),
MeasureTheory.Integrable
(fun (v : Fin (2 * q - 2) → T4) =>
detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure)) →
|endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z| ≤ primitiveKernelMajorant primitiveConstant lam ε supportConstant q z
Uniform fixed-signature majorant whose exact identity and quantitative terminal estimate are proved on one aligned terminal context.
theorem
Anderson4D.R322AnalyticResidualPrefix.exists_r322AnalyticAlignedEndpointMajorantAE
(ρ : SmoothCutoff)
:
∃ (supportConstant : ℝ) (primitiveConstant : ℝ),
0 < supportConstant ∧ 0 < primitiveConstant ∧ ∀ (lam ε : ℝ) (q : ℕ),
1 ≤ q →
∀ κ ∈ nonSplitPairings q,
0 < lam →
0 < ε →
ε ≤ 1 →
1 ≤ |Real.log ε| →
q ≤ truncOrder ε →
∀ᵐ (z : T4) ∂paperMeasure, |endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z| ≤ primitiveKernelMajorant primitiveConstant lam ε supportConstant q z
The production fixed-signature bound in the strength actually needed
by the downstream spatial integral. The internal section premise is
discharged from joint frozen-J integrability, hence the honest conclusion
is almost everywhere in the external endpoint.
Almost-everywhere numerical closure #
def
Anderson4D.R322AnalyticResidualPrefix.RenormFiberReductionOutputAE
(ρ : SmoothCutoff)
(lam ε : ℝ)
(q : ℕ)
(primitiveConstant supportConstant : ℝ)
:
Fixed-signature reduction output at the exact strength consumed by the spatial integral.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Anderson4D.R322AnalyticResidualPrefix.RenormReductionOutputAE
(ρ : SmoothCutoff)
(lam ε : ℝ)
(q : ℕ)
(primitiveConstant supportConstant : ℝ)
:
Grouped reduction output with an almost-everywhere spatial bound.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R322AnalyticResidualPrefix.RenormFiberReductionOutputAE.toRenormReductionOutputAE
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{primitiveConstant supportConstant : ℝ}
(hC : 0 ≤ primitiveConstant)
(hlam : 0 ≤ lam)
(hred : RenormFiberReductionOutputAE ρ lam ε q primitiveConstant supportConstant)
:
RenormReductionOutputAE ρ lam ε q (4 * primitiveConstant) supportConstant
Summing the finite endpoint signatures preserves an a.e. estimate and
costs the same 4^(2q) factor as the pointwise interface.
theorem
Anderson4D.R322AnalyticResidualPrefix.exists_r322RenormFiberReductionOutputAE
(ρ : SmoothCutoff)
:
The aligned analytic construction supplies the complete fixed-signature a.e. reduction package, including the independent integrability field.
theorem
Anderson4D.R322AnalyticResidualPrefix.abs_renormC2q_le_integral_primitiveKernelMajorant_of_ae
{ρ : SmoothCutoff}
{lam ε : ℝ}
{q : ℕ}
{primitiveConstant supportConstant : ℝ}
(hε : 0 < ε)
(hred : RenormReductionOutputAE ρ lam ε q primitiveConstant supportConstant)
:
|renormC2q ρ lam ε q| ≤ ∫ (z : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant q z ∂paperMeasure
An a.e. grouped majorant controls the renormalization constant by the same majorant integral as the stronger pointwise interface.
Uniform numerical closure #
theorem
Anderson4D.R322AnalyticResidualPrefix.exists_abs_renormC2q_le_raw_of_ae :
∃ (Cball : ℝ) (Creg : ℝ),
0 < Cball ∧ 0 < Creg ∧ ∀ (ρ : SmoothCutoff) (primitiveConstant supportConstant lam ε : ℝ) (q : ℕ),
0 < ε →
0 < supportConstant →
1 ≤ |Real.log ε| →
RenormReductionOutputAE ρ lam ε q primitiveConstant supportConstant →
|renormC2q ρ lam ε q| ≤ (primitiveConstant * lam) ^ (2 * q) * ((Cball * supportConstant ^ 2 + Creg) * ε⁻¹ ^ 2 / |Real.log ε|)
Raw integrated form of (4.15) from the honest almost-everywhere reduction output. The integration constants are chosen independently of the cutoff, coupling, scale, perturbative order, and primitive constant.
theorem
Anderson4D.R322AnalyticResidualPrefix.exists_renormC_bound_of_reduction_ae
{primitiveConstant supportConstant : ℝ}
(hprimitive : 0 < primitiveConstant)
(hsupport : 0 < supportConstant)
:
Numerical closure of R-322 for the almost-everywhere reduction
interface. One positive constant is chosen before ρ, λ, ε, and q;
all order-independent integration losses are absorbed into the base of the
even power.
Constructive R-322, paper (3.22).
For a fixed cutoff, the exact residual iteration, its quantitative terminal
estimate, the almost-everywhere section argument, endpoint-signature
aggregation, spatial integration, and numerical absorption close to one
all-order theorem. The named constant is uniform in λ, ε, and q.
The logarithmic lower bound is derived from
1 ≤ q ≤ truncOrder ε, rather than exposed as an extra hypothesis.
theorem
Anderson4D.R322AnalyticResidualPrefix.exists_terminalContext_endpointFiberDetJSum_eq
(ρ : SmoothCutoff)
(lam ε : ℝ)
{q : ℕ}
(hq : 1 ≤ q)
(κ : PartialPairing (Fin (2 * q)))
(hκ : κ ∈ nonSplitPairings q)
(z : T4)
(hlam : 0 < lam)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(hlog : 1 ≤ |Real.log ε|)
(hqtrunc : q ≤ truncOrder ε)
(hint :
∀ (τ : ReductionEndpointFiberAt κ),
MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure))
:
∃ (ctx : R322AnalyticTerminalStepContext q hq),
endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = ctx.terminalSpatialIntegral ρ lam ε z 0
Complete exact R-322 iteration along the canonical proper prefix. The terminal context is produced by the same residual run that proves the identity, so no equality between independently selected terminal states is assumed.