Numerical closure of paper Step 4(A)

After all signed primitive removals and the four endpoint integrations, the physical argument leaves one inserted primitive majorant at the ambient order, together with the four ordinary-J endpoint sacrifices. Each sacrifice costs at most epsilon^(-2), so the producer boundary retains the paper's total epsilon^(-8) loss explicitly. This file performs only the final scalar calculation: divide out the full |lambda_epsilon|^(2m) weight, integrate the majorant, and absorb its order-independent mass into one geometric base.

There is no physical integral, pairing sum, or triangle inequality here.

def Anderson4D.R324PaperEndpointWeightedMajorantBound (rho : SmoothCutoff) (primitiveConstant supportConstant : ℝ) : Prop

The exact paper-facing producer boundary after all signed removals and four endpoint integrations. It deliberately retains the complete |lambda_epsilon|^(2m) weight and the final inserted majorant.

Equations

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

theorem Anderson4D.exists_r324PaperEndpointBase_of_weightedMajorant (rho : SmoothCutoff) {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ {epsilon : ℝ} (m : ℕ) (alpha beta : Z4), 0 < epsilon → epsilon ≤ 1 / 4 → 1 ≤ |Real.log epsilon| → 2 ≤ m → m ≤ truncOrder epsilon → ∀ (p : R324RefinedScheduleIndex m), |lamEps 1 epsilon| ^ (2 * m) * ‖r324RefinedPhysicalIntegral rho epsilon m alpha beta p‖ ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (epsilon⁻¹ ^ 8 * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant 1 epsilon supportConstant m z ∂paperMeasure) → ‖r324RefinedPhysicalIntegral rho epsilon m alpha beta p‖ ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (↑m ^ 8 * K ^ m * |Real.log epsilon| ^ (m - 1) * epsilon⁻¹ ^ 8)

A complete weighted endpoint-to-majorant estimate implies the literal Step 4(A) physical bound. This is the common numerical consumer for the full/full and residual endpoint case splits.

theorem Anderson4D.R324PaperEndpointWeightedMajorantBound.toPhysicalBound {rho : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (h : R324PaperEndpointWeightedMajorantBound rho primitiveConstant supportConstant) : ∃ (K : ℝ), 0 < K ∧ R324PaperEndpointPhysicalBound rho K

Packaging the preceding scalar lemma: a uniform weighted-majorant producer closes Step 4(A) with one positive geometric base.