Common weighted exit for the actual two-half endpoint table #
The four endpoint routes have already been evaluated, composed, and then estimated before this file is used. The only extra scalar in their common majorant is the fixed, route-independent endpoint-mass compensation. This file absorbs that scalar into the primitive base and invokes the existing complete-run exit; it introduces no new spatial or combinatorial carrier.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.twoHalfEndpointCompleteAbsorbedBase
(A C K B : ℝ)
:
Complete-run base after absorbing the single fixed scalar shared by all sixteen literal endpoint patterns.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.weighted_norm_le_endpointPatternAmbientMajorant_of_grouped_uniform
{rho : SmoothCutoff}
{C K A B lam eps supportConstant : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{leftMode rightMode : Z4}
{leftProviders : R324PaperHalfRouteProviders kappaP leftMode}
{rightProviders : R324PaperHalfRouteProviders kappaM rightMode}
(routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders)
(hA : 0 ≤ A)
(hC : 0 ≤ C)
(hK : 0 ≤ K)
(hB : 0 ≤ B)
(hlam : 0 < lam)
(hleft : routes.terminal.left.state.active.Nonempty)
(hright : routes.terminal.right.state.active.Nonempty)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(head : R324NestedCrossBlock kappaP kappaM pi)
(tail : List (R324NestedCrossBlock kappaP kappaM pi))
(hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail)
(alpha beta : Z4)
(physical : ℂ)
(endpointDensity : (routes.terminal.NestedCoordinate pi → T4) → ℂ)
(hendpoint :
(fun (v : routes.terminal.NestedCoordinate pi → T4) =>
‖endpointDensity v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : routes.terminal.NestedCoordinate pi) => paperMeasure] fun (v : routes.terminal.NestedCoordinate pi → T4) =>
R324PaperHalfEndpointUniformBound.twoHalfEndpointMassCompensation * (paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps routes.cases) * routes.terminal.initialNestedEndpointIntegratedGroupedMajorant routes.left.completedRoute.terminalScale
routes.right.completedRoute.terminalScale hleft hright pi v)
(heps : 0 < eps)
(heps1 : eps ≤ 1)
(hlog : 1 ≤ |Real.log eps|)
(hm : 1 ≤ m)
(hmtrunc : m ≤ truncOrder eps)
(hrunBound :
let step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining;
have hleftInitial := ⋯;
have hrightInitial := ⋯;
(∫ (v : step.SurvivingCoordinate → T4), routes.terminal.completeNestedRunDensity step hleftInitial hrightInitial
v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant B lam eps supportConstant step.residual.remainingOrder z ∂paperMeasure)
(horder :
(initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder + (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remainingOrder = m)
(hcollapse :
↑(lamEps lam eps) ^ (2 * ((initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder)) * physical = ∫ (v : routes.terminal.NestedCoordinate pi → T4), endpointDensity v ∂MeasureTheory.Measure.pi fun (x : routes.terminal.NestedCoordinate pi) => paperMeasure)
:
|lamEps lam eps| ^ (2 * m) * ‖physical‖ ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps routes.cases * ∫ (z : T4), primitiveInsertedMajorant (twoHalfEndpointCompleteAbsorbedBase A C K B) lam eps supportConstant m
z ∂paperMeasure)
Numerical Step 4(A) exit for the common route-independent endpoint compensation. The endpoint density is already the result of all four signed operations, so this theorem is the first place where its norm is used.