Concrete Phase-A trace assembly for R-324 #
This file closes two local gaps at the entrance to the physical R-324 collapse.
- Proposition 4.1 at the actual truncation constructs the two endpoint-independent certified within-half traces from the all-Green initial states.
- Full integrability at the root of a certified trace propagates through
every genuine head. Consequently the two
WeightedIntegrableAlonghypotheses used by the exact two-half collapse follow from one left-section premise and the genuine joint root integrability.
The two remaining premises in the last theorem are literal integrability statements for the uncollapsed physical density. They do not assert a moment estimate or a target-shaped bound.
Proposition 4.1 constructs both certified within-half traces #
theorem
Anderson4D.R324WithinHalfStepContext.order_le_ambient
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(ctx : R324WithinHalfStepContext pairing)
:
Every literal within-half block has order at most the ambient perturbative order.
The proved truncation form of Proposition 4.1 supplies a complete local block provider for either within-half pairing.
theorem
Anderson4D.exists_r324InitialCertifiedAnalyticTraces_at_truncation
(ρ : SmoothCutoff)
:
∃ (supportConstant : ℝ) (C : ℝ) (K : ℝ) (A : ℝ),
0 < supportConstant ∧ 0 < C ∧ 0 < K ∧ 1 ≤ A ∧ ∀ (lam ε : ℝ) (m : ℕ) (κp κm : PartialPairing (Fin m)),
0 < lam →
0 < ε →
ε ≤ 1 →
1 ≤ |Real.log ε| →
m ≤ truncOrder ε →
Nonempty
(((R324WithinHalfResidualPrefix.initial ρ lam ε κp).R324WithinHalfCertifiedAnalyticTrace
fun (x : Fin (m + 1)) => A) × (R324WithinHalfResidualPrefix.initial ρ lam ε κm).R324WithinHalfCertifiedAnalyticTrace
fun (x : Fin (m + 1)) => A)
Concrete simultaneous construction of the two endpoint-independent certified traces used by the R-324 two-half bridge.
All numerical constants are selected before the ambient order and the two
pairings. The only analytic input is the already proved
proposition41_at_truncation.
The honest terminal case of the nested physical factorization #
noncomputable def
Anderson4D.R324InitialNestedContextFactorization.of_initial_marked_head
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
{selected : R324ResidualCovarianceSlot κp}
{terminal : R324TwoHalfTerminalData ρ lam ε κp κm}
{L : ℝ}
{x y z w : T4}
(head : R324NestedCrossBlock κp κm π)
(tail : List (R324NestedCrossBlock κp κm π))
(hremaining : (R324NestedCrossResidualPrefix.initial κp κm π).remaining = head :: tail)
(hhead : head.carrier = r324MarkedResidualBlock κp κm π selected)
(hphysical :
MeasureTheory.Integrable (terminal.initialNestedMarkedPhysicalCore π selected L x y z w)
(MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure))
:
R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w
If the marked carrier is already the literal first cross block, the physical norm boundary itself is the terminal context factorization.
This constructor is restricted to that terminal case. A marked carrier deeper in the schedule uses the preceding-block factorization hypothesis; the canonical proper-prefix run alone does not provide that comparison.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Weighted integrability propagates from one honest root premise #
theorem
Anderson4D.R324WithinHalfResidualPrefix.integrable_residualIntegrand_mul_postOuter_afterHead
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(head : R322ExtractionStep m)
(tail : List (R322ExtractionStep m))
(hremaining : res.remaining = head :: tail)
(x y : T4)
(postOuter : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ)
(hfull :
MeasureTheory.Integrable
(fun (w : res.SurvivingCoordinate → T4) =>
↑(res.residualIntegrand ρ ε x y (res.reconstruct w)) * postOuter ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2)
(MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))
(hinternal :
∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))),
MeasureTheory.Integrable
(fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB)
(res.headContext head tail hremaining).internalEdges
(primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure))
:
MeasureTheory.Integrable
(fun (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) =>
↑((res.afterHead head tail hremaining).residualIntegrand ρ ε x y
((res.afterHead head tail hremaining).reconstruct v)) * postOuter v)
(MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure)
Full integrability with an arbitrary post-coordinate outer function is preserved by one certified head collapse.
This is the weighted counterpart of
integrable_residualIntegrand_afterHead; crucially, it never cancels the
outer factor on its zero set.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.weightedIntegrableAlong_of_integrable
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
{scale : Fin (m + 1) → ℝ}
(x y : T4)
(trace : res.R324WithinHalfCertifiedAnalyticTrace scale)
(outer : (trace.terminalPrefix.SurvivingCoordinate → T4) → ℂ)
(hroot :
MeasureTheory.Integrable
(fun (v : res.SurvivingCoordinate → T4) =>
↑(res.residualIntegrand ρ ε x y (res.reconstruct v)) * outer (trace.terminalProjection v))
(MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))
:
WeightedIntegrableAlong x y trace outer
A single honest weighted-integrability premise at the root propagates through every scalar integral traversed by a certified trace.
The two weighted hypotheses from root physical integrability #
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.twoHalf_weightedIntegrableAlong_of_root_integrable
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{x y z w : T4}
{leftRes : R324WithinHalfResidualPrefix ρ lam ε κp}
{rightRes : R324WithinHalfResidualPrefix ρ lam ε κm}
{leftScale rightScale : Fin (m + 1) → ℝ}
(leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftScale)
(rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightScale)
(cross : (leftTrace.terminalPrefix.SurvivingCoordinate → T4) → (rightTrace.terminalPrefix.SurvivingCoordinate → T4) → ℂ)
(hleftRoot :
∀ᵐ (vr :
rightRes.SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : rightRes.SurvivingCoordinate) => paperMeasure, MeasureTheory.Integrable
(fun (vl : leftRes.SurvivingCoordinate → T4) =>
↑(leftRes.residualIntegrand ρ ε x y (leftRes.reconstruct vl)) * cross (leftTrace.terminalProjection vl) (rightTrace.terminalProjection vr))
(MeasureTheory.Measure.pi fun (x : leftRes.SurvivingCoordinate) => paperMeasure))
(hjoint :
MeasureTheory.Integrable
(fun (p : (leftRes.SurvivingCoordinate → T4) × (rightRes.SurvivingCoordinate → T4)) =>
↑(leftRes.residualIntegrand ρ ε x y (leftRes.reconstruct p.1)) * (↑(rightRes.residualIntegrand ρ ε z w (rightRes.reconstruct p.2)) * cross (leftTrace.terminalProjection p.1) (rightTrace.terminalProjection p.2)))
((MeasureTheory.Measure.pi fun (x : leftRes.SurvivingCoordinate) => paperMeasure).prod
(MeasureTheory.Measure.pi fun (x : rightRes.SurvivingCoordinate) => paperMeasure)))
:
(∀ᵐ (vr :
rightRes.SurvivingCoordinate → T4) ∂MeasureTheory.Measure.pi fun (x : rightRes.SurvivingCoordinate) => paperMeasure, WeightedIntegrableAlong x y leftTrace fun (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4) =>
cross vl (rightTrace.terminalProjection vr)) ∧ WeightedIntegrableAlong z w rightTrace fun (vr : rightTrace.terminalPrefix.SurvivingCoordinate → T4) =>
∫ (vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4), ↑(leftTrace.terminalPrefix.residualIntegrand ρ ε x y (leftTrace.terminalPrefix.reconstruct vl)) * cross vl vr ∂MeasureTheory.Measure.pi fun (x : leftTrace.terminalPrefix.SurvivingCoordinate) => paperMeasure
The exact WeightedIntegrableAlong hypotheses for the two-half
collapse follow from:
- integrability of the genuine left section for almost every right configuration; and
- joint integrability of the genuine uncollapsed two-half density.
These are root-level physical integrability statements, not recursive providers and not quantitative bounds.