Uniform two-half endpoint majorant

This is the numerical Step 4(A) seam for the common ordered endpoint product. The right uniform estimate is applied first. Its coefficient is the already completed left density; the left uniform estimate is then applied to that coefficient with the untouched residual primitive factor. Thus all four signed endpoint operations have already occurred before this file takes a norm.

The proof keeps the two literal outgoing endpoint masses until the final comparison with the four-mass grouped carrier. That comparison uses only a route-dependent, perturbative-order-independent scalar. There is no case split and no new residual sum or scale ledger.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.twoHalfOutgoingEndpointMass {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP alpha} {rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)} (routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders) : ℝ

The exact product of the two literal outgoing endpoint masses.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.twoHalfOutgoingEndpointMassCap : ℝ

A route-independent cap for either literal outgoing endpoint mass.

Equations

• Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.twoHalfOutgoingEndpointMassCap = max 1 Anderson4D.invSqKerMass

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.twoHalfEndpointMassCompensation : ℝ

The sole enlargement needed to exchange either possible product of literal outgoing masses for invSqKerMass ^ 4. It is independent of both the endpoint route and perturbative order.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.one_le_twoHalfEndpointMassCompensation : 1 ≤ twoHalfEndpointMassCompensation

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointUniformBound.ae_norm_nestedEndpointProductDensity_le_compensatedGrouped {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha beta : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP alpha} {rightProviders : R324PaperHalfRouteProviders kappaM (-alpha)} (routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders) (left : R324PaperHalfEndpointUniformBound routes.left.completedRoute) (right : R324PaperHalfEndpointUniformBound routes.right.completedRoute) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) : (fun (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4) => ‖left.nestedEndpointProductDensity right beta pi v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : (left.twoHalfTerminal right).NestedCoordinate pi) => paperMeasure] fun (v : (left.twoHalfTerminal right).NestedCoordinate pi → T4) => twoHalfEndpointMassCompensation * (paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps routes.cases) * (left.twoHalfTerminal right).initialNestedEndpointIntegratedGroupedMajorant routes.left.completedRoute.terminalScale routes.right.completedRoute.terminalScale ⋯ ⋯ pi v

The generic two-half endpoint exit. It is the only theorem in this file intended for the residual producer: the ordered signed endpoint density is reindexed from product Haar to the common nested terminal and dominated there by the existing initialNestedEndpointIntegratedGroupedMajorant. The producer may use twoHalfTerminal_eq_routes once to identify this carrier with routes.terminal.