Honest physical-to-canonical boundary for the initial R-324 cross suffix #
The exact two-half bridge ends with a complex physical core on the literal initial nested carrier. The proper cross-prefix iteration, by contrast, consumes a nonnegative canonical majorant and stops at the block containing the selected projected covariance.
This file records the missing boundary without identifying those two objects pointwise:
- the physical core is first replaced by its norm;
- the exact residual perturbative weight is kept on that norm;
- every unmarked proper head is exposed explicitly as
normalizedHeadDensity * connector * nextMajorant; - the stop constructor retains an arbitrary four-endpoint context with the actual named endpoints; and
- every physical comparison is stated almost everywhere, because the
inserted
distance² * invSqKercancellation is false on the totalized diagonal.
Thus a value of R324InitialNestedContextFactorization is a local,
proof-relevant factorization certificate. It is not a target-shaped
pointwise density hypothesis and it does not discard the Step 4 endpoint
payload.
The correctly weighted physical norm boundary #
noncomputable def
Anderson4D.R324TwoHalfTerminalData.initialNestedWeightedNormDensity
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(π : ↥κp.singles ≃ ↥κm.singles)
(selected : R324ResidualCovarianceSlot κp)
(L : ℝ)
(x y z w : T4)
(v : terminal.NestedCoordinate π → T4)
:
The physical norm density with exactly the perturbative weight carried by the initial residual cross schedule. In particular, the weight is not silently charged to the already completed within-half schedules.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324TwoHalfTerminalData.initialNestedWeightedNormDensity_nonneg
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(π : ↥κp.singles ≃ ↥κm.singles)
(selected : R324ResidualCovarianceSlot κp)
(L : ℝ)
(x y z w : T4)
(v : terminal.NestedCoordinate π → T4)
:
theorem
Anderson4D.R324TwoHalfTerminalData.initialNestedWeightedNormDensity_eq_absWeight
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(π : ↥κp.singles ≃ ↥κm.singles)
(selected : R324ResidualCovarianceSlot κp)
(L : ℝ)
(x y z w : T4)
(v : terminal.NestedCoordinate π → T4)
:
terminal.initialNestedWeightedNormDensity π selected L x y z w v = |lamEps lam ε| ^ (2 * (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder) * terminal.initialNestedMarkedNormDensity π selected L x y z w v
Absolute-value spelling of the same weight. The equality uses only that the perturbative exponent is even.
theorem
Anderson4D.R324TwoHalfTerminalData.integrable_initialNestedWeightedNormDensity
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(π : ↥κp.singles ≃ ↥κm.singles)
(selected : R324ResidualCovarianceSlot κp)
(L : ℝ)
(x y z w : T4)
(hphysical :
MeasureTheory.Integrable (terminal.initialNestedMarkedPhysicalCore π selected L x y z w)
(MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure))
:
MeasureTheory.Integrable (terminal.initialNestedWeightedNormDensity π selected L x y z w)
(MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure)
theorem
Anderson4D.R324TwoHalfTerminalData.initialWeight_mul_norm_integral_le_integral_weightedNorm
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(π : ↥κp.singles ≃ ↥κm.singles)
(selected : R324ResidualCovarianceSlot κp)
(L : ℝ)
(x y z w : T4)
:
lamEps lam ε ^ (2 * (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder) * ‖∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedMarkedPhysicalCore π selected L x y z w
v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure‖ ≤ ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedWeightedNormDensity π selected L x y z w
v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure
The weighted physical integral is bounded by the integral of the weighted norm density. This is the last statement which does not mention any canonical proper-prefix majorant.
theorem
Anderson4D.R324TwoHalfTerminalData.absInitialWeight_mul_norm_integral_le_integral_weightedNorm
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(π : ↥κp.singles ≃ ↥κm.singles)
(selected : R324ResidualCovarianceSlot κp)
(L : ℝ)
(x y z w : T4)
:
|lamEps lam ε| ^ (2 * (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder) * ‖∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedMarkedPhysicalCore π selected L x y z w
v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure‖ ≤ ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedWeightedNormDensity π selected L x y z w
v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure
Absolute-value form of the weighted integral boundary.
theorem
Anderson4D.R324TwoHalfTerminalData.norm_complexInitialWeight_mul_integral_eq
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(π : ↥κp.singles ≃ ↥κm.singles)
(selected : R324ResidualCovarianceSlot κp)
(L : ℝ)
(x y z w : T4)
:
‖↑(lamEps lam ε) ^ (2 * (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder) * ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedMarkedPhysicalCore π selected L x y z w
v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure‖ = lamEps lam ε ^ (2 * (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder) * ‖∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedMarkedPhysicalCore π selected L x y z w
v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure‖
Norm of the genuinely complex perturbative weight. This equality is the bridge between the complex coefficient identity and the real nonnegative factorization below.
theorem
Anderson4D.R324TwoHalfTerminalData.norm_complexInitialWeight_mul_integral_le_integral_weightedNorm
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(π : ↥κp.singles ≃ ↥κm.singles)
(selected : R324ResidualCovarianceSlot κp)
(L : ℝ)
(x y z w : T4)
:
‖↑(lamEps lam ε) ^ (2 * (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder) * ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedMarkedPhysicalCore π selected L x y z w
v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure‖ ≤ ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedWeightedNormDensity π selected L x y z w
v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure
Direct complex-weight form of the physical-to-weighted-norm boundary.
An endpoint-preserving local factorization certificate #
@[simp]
theorem
Anderson4D.R324NestedCrossTerminalPayload.ofContext_unscaledDensity
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(lam ε : ℝ)
(step : R324NestedCrossStepContext κp κm π)
(context : T4 → T4 → T4 → T4 → (step.SurvivingCoordinate → T4) → ℝ)
(x y z w : T4)
:
@[simp]
theorem
Anderson4D.R324NestedCrossTerminalPayload.ofContext_density
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(lam ε : ℝ)
(step : R324NestedCrossStepContext κp κm π)
(context : T4 → T4 → T4 → T4 → (step.SurvivingCoordinate → T4) → ℝ)
(x y z w : T4)
:
theorem
Anderson4D.R324NestedCrossStepContext.ae_post_comp_le
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ctx : R324NestedCrossStepContext κp κm π)
{f g : (ctx.PostCoordinate → T4) → ℝ}
(hfg : f ≤ᵐ[MeasureTheory.Measure.pi fun (x : ctx.PostCoordinate) => paperMeasure] g)
:
(fun (v : ctx.SurvivingCoordinate → T4) =>
f fun (i : ctx.PostCoordinate) =>
v (ctx.postSurvivingCoordinate i)) ≤ᵐ[MeasureTheory.Measure.pi fun (x : ctx.SurvivingCoordinate) => paperMeasure] fun (v : ctx.SurvivingCoordinate → T4) => g fun (i : ctx.PostCoordinate) => v (ctx.postSurvivingCoordinate i)
Pull an a.e. comparison on the next suffix back to the current surviving carrier. This is the measure-theoretic step needed to compose honest one-head comparisons; it is not an additional majorization hypothesis.
inductive
Anderson4D.R324NestedCrossContextFactorization
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
(ρ : SmoothCutoff)
(lam ε : ℝ)
(stopCarrier : Finset (Fin (2 * m)))
(x y z w : T4)
(res : R324NestedCrossResidualPrefix κp κm π)
:
((↥res.activeCarrier → T4) → ℝ) → ((↥res.activeCarrier → T4) → ℝ) → ℕ → ℕ → Prop
A local, a.e. physical factorization along the proper prefix before a chosen stop carrier.
The source field is the physical density still to be controlled at the
current suffix. The majorant field is forced constructor-by-constructor
to be the canonical run density. At stop, its context still receives
all four external endpoints. Integrability is stored recursively so every
suffix needed by the later Bochner/Fubini iteration is available.
- stop {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {x y z w : T4} (step : R324NestedCrossStepContext κp κm π) (hstop : step.head.carrier = stopCarrier) (context : T4 → T4 → T4 → T4 → (step.SurvivingCoordinate → T4) → ℝ) (source : (step.SurvivingCoordinate → T4) → ℝ) (hcontext : ∀ (v : step.SurvivingCoordinate → T4), 0 ≤ context x y z w v) (hmajorant : MeasureTheory.Integrable (R324NestedCrossTerminalPayload.ofContext lam ε step context x y z w).density (MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure)) (hle : source ≤ᵐ[MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure] (R324NestedCrossTerminalPayload.ofContext lam ε step context x y z w).density) : R324NestedCrossContextFactorization ρ lam ε stopCarrier x y z w step.residual source (R324NestedCrossTerminalPayload.ofContext lam ε step context x y z w).density 0 step.residual.remainingOrder
- proper {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} {ρ : SmoothCutoff} {lam ε : ℝ} {stopCarrier : Finset (Fin (2 * m))} {x y z w : T4} (ctx : R324NestedCrossProperStepContext κp κm π) (hhead : ctx.step.head.carrier ≠ stopCarrier) (source : (ctx.step.SurvivingCoordinate → T4) → ℝ) (nextSource nextMajorant : (ctx.step.PostCoordinate → T4) → ℝ) (nextPrefixOrder terminalOrder : ℕ) (next : R324NestedCrossContextFactorization ρ lam ε stopCarrier x y z w ctx.step.next nextSource nextMajorant nextPrefixOrder terminalOrder) (hle : source ≤ᵐ[MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure] fun (v : ctx.step.SurvivingCoordinate → T4) => ((ctx.step.normalizedHeadDensity ρ lam ε fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) * ctx.connector (fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) * nextSource fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) (hmajorant : MeasureTheory.Integrable (fun (v : ctx.step.SurvivingCoordinate → T4) => ((ctx.step.normalizedHeadDensity ρ lam ε fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) * ctx.connector (fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) * nextMajorant fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) (MeasureTheory.Measure.pi fun (x : ctx.step.SurvivingCoordinate) => paperMeasure)) : R324NestedCrossContextFactorization ρ lam ε stopCarrier x y z w ctx.step.residual source (fun (v : ↥ctx.step.residual.activeCarrier → T4) => ((ctx.step.normalizedHeadDensity ρ lam ε fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) * ctx.connector (fun (j : Fin (2 * ctx.step.order)) => v (ctx.step.headSurvivingCoordinate j)) fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) * nextMajorant fun (i : ctx.step.PostCoordinate) => v (ctx.step.postSurvivingCoordinate i)) (ctx.step.order + nextPrefixOrder) terminalOrder
Instances For
theorem
Anderson4D.R324NestedCrossContextFactorization.toProperPrefixRun
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
{ρ : SmoothCutoff}
{lam ε : ℝ}
{stopCarrier : Finset (Fin (2 * m))}
{x y z w : T4}
{res : R324NestedCrossResidualPrefix κp κm π}
{source majorant : (↥res.activeCarrier → T4) → ℝ}
{prefixOrder terminalOrder : ℕ}
(factorization :
R324NestedCrossContextFactorization ρ lam ε stopCarrier x y z w res source majorant prefixOrder terminalOrder)
:
R324NestedCrossProperPrefixRun ρ lam ε stopCarrier res majorant prefixOrder terminalOrder
Forgetting the physical comparison leaves exactly the canonical proper-prefix run consumed by the cross iteration.
theorem
Anderson4D.R324NestedCrossContextFactorization.ae_le
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
{ρ : SmoothCutoff}
{lam ε : ℝ}
{stopCarrier : Finset (Fin (2 * m))}
{x y z w : T4}
{res : R324NestedCrossResidualPrefix κp κm π}
{source majorant : (↥res.activeCarrier → T4) → ℝ}
{prefixOrder terminalOrder : ℕ}
(factorization :
R324NestedCrossContextFactorization ρ lam ε stopCarrier x y z w res source majorant prefixOrder terminalOrder)
:
source ≤ᵐ[MeasureTheory.Measure.pi fun (x : ↥res.activeCarrier) => paperMeasure] majorant
The source-to-majorant comparison obtained by composing the honest one-head comparison with the recursively generated next-suffix comparison.
theorem
Anderson4D.R324NestedCrossContextFactorization.majorant_integrable
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
{ρ : SmoothCutoff}
{lam ε : ℝ}
{stopCarrier : Finset (Fin (2 * m))}
{x y z w : T4}
{res : R324NestedCrossResidualPrefix κp κm π}
{source majorant : (↥res.activeCarrier → T4) → ℝ}
{prefixOrder terminalOrder : ℕ}
(factorization :
R324NestedCrossContextFactorization ρ lam ε stopCarrier x y z w res source majorant prefixOrder terminalOrder)
:
MeasureTheory.Integrable majorant (MeasureTheory.Measure.pi fun (x : ↥res.activeCarrier) => paperMeasure)
Integrability is retained at every suffix, not merely at the initial carrier. This is the recursive datum required by the proper-head Bochner/Fubini iteration.
theorem
Anderson4D.R324NestedCrossContextFactorization.majorant_nonneg
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{π : ↥κp.singles ≃ ↥κm.singles}
{ρ : SmoothCutoff}
{lam ε : ℝ}
{stopCarrier : Finset (Fin (2 * m))}
{x y z w : T4}
{res : R324NestedCrossResidualPrefix κp κm π}
{source majorant : (↥res.activeCarrier → T4) → ℝ}
{prefixOrder terminalOrder : ℕ}
(factorization :
R324NestedCrossContextFactorization ρ lam ε stopCarrier x y z w res source majorant prefixOrder terminalOrder)
(v : ↥res.activeCarrier → T4)
:
Every canonical majorant produced by the certificate is pointwise nonnegative.
The initial package and its integral-level consumer #
structure
Anderson4D.R324InitialNestedContextFactorization
(ρ : 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)
:
Complete factorization datum at the output of the exact two-half bridge, including the local certificate and its suffix-by-suffix integrability data.
- majorant : (terminal.NestedCoordinate π → T4) → ℝ
- prefixOrder : ℕ
- terminalOrder : ℕ
- factorization : R324NestedCrossContextFactorization ρ lam ε (r324MarkedResidualBlock κp κm π selected) x y z w (R324NestedCrossResidualPrefix.initial κp κm π) (terminal.initialNestedWeightedNormDensity π selected L x y z w) self.majorant self.prefixOrder self.terminalOrder
Instances For
theorem
Anderson4D.R324InitialNestedContextFactorization.toProperPrefixRun
{ρ : 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}
(factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w)
:
R324NestedCrossProperPrefixRun ρ lam ε (r324MarkedResidualBlock κp κm π selected)
(R324NestedCrossResidualPrefix.initial κp κm π) factorization.majorant factorization.prefixOrder
factorization.terminalOrder
The packaged majorant carries the canonical stop-at-marked run.
theorem
Anderson4D.R324InitialNestedContextFactorization.majorant_integrable
{ρ : 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}
(factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w)
:
MeasureTheory.Integrable factorization.majorant
(MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure)
Initial-carrier integrability, projected from the recursive suffix-by-suffix certificate.
theorem
Anderson4D.R324InitialNestedContextFactorization.majorant_nonneg
{ρ : 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}
(factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w)
(v : terminal.NestedCoordinate π → T4)
:
Initial canonical majorant is pointwise nonnegative.
theorem
Anderson4D.R324InitialNestedContextFactorization.prefixOrder_add_terminalOrder
{ρ : 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}
(factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w)
:
factorization.prefixOrder + factorization.terminalOrder = (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder
The exact perturbative weight splits into the proper-prefix order and the terminal marked/suffix order recorded by the canonical run.
theorem
Anderson4D.R324InitialNestedContextFactorization.initialWeight_mul_norm_integral_le_majorant
{ρ : 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}
(factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w)
(hphysical :
MeasureTheory.Integrable (terminal.initialNestedMarkedPhysicalCore π selected L x y z w)
(MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure))
:
lamEps lam ε ^ (2 * (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder) * ‖∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedMarkedPhysicalCore π selected L x y z w
v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure‖ ≤ ∫ (v : terminal.NestedCoordinate π → T4), factorization.majorant v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure
Main integral-level handoff. It keeps the four external endpoints in the terminal payload while allowing every earlier proper block to be consumed by the canonical cross iteration.
theorem
Anderson4D.R324InitialNestedContextFactorization.norm_complexInitialWeight_mul_integral_le_majorant
{ρ : 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}
(factorization : R324InitialNestedContextFactorization ρ lam ε κp κm π selected terminal L x y z w)
(hphysical :
MeasureTheory.Integrable (terminal.initialNestedMarkedPhysicalCore π selected L x y z w)
(MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure))
:
‖↑(lamEps lam ε) ^ (2 * (R324NestedCrossResidualPrefix.initial κp κm π).remainingOrder) * ∫ (v : terminal.NestedCoordinate π → T4), terminal.initialNestedMarkedPhysicalCore π selected L x y z w
v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure‖ ≤ ∫ (v : terminal.NestedCoordinate π → T4), factorization.majorant v ∂MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate π) => paperMeasure
Consumer-facing complex form of the same endpoint-preserving handoff.