Paper Step 4(A) before the central-frequency case split

The four endpoint integrations in paper Section 4.2, Step 4 do not assume that the conserved shift alpha + beta vanishes. The old zero-shift interface is only the branch in which the central-frequency argument is unnecessary. This file records the stronger, literal endpoint statement.

Keeping this distinction is useful in the complementary branch epsilon^2 * |alpha + beta| < 1: there the eighth-order central bracket is bounded below by an absolute constant, so Step 4(A) already gives the full paper bound and no first-high selector is needed.

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

The exact endpoint-to-majorant producer, for arbitrary external modes. All primitive removals precede the norm, exactly as in paper Step 2(f).

Equations

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

def Anderson4D.R324PaperEndpointAllShiftPhysicalBound (rho : SmoothCutoff) (K : ℝ) : Prop

The arbitrary-shift endpoint estimate after the common numerical conversion of the final inserted primitive majorant.

Equations

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

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

The scalar endpoint-majorant calculation is independent of the conserved shift, so it packages the stronger producer without change.

theorem Anderson4D.R324PaperEndpointAllShiftPhysicalBound.toZeroShift {rho : SmoothCutoff} {K : ℝ} (h : R324PaperEndpointAllShiftPhysicalBound rho K) : R324PaperEndpointPhysicalBound rho K

The old zero-shift endpoint interface is a direct specialization.