Paper Step 4(A) consumer at zero conserved shift

The four external variables in (4.18) are integrated before the first norm. This file records only the final cancellation of their strictly positive Fourier multipliers. The analytic producer belongs to the endpoint-collapse modules: it must first finish every primitive-interval removal and may then pay at most one ordinary-J sacrifice at each external endpoint.

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

The paper Step 4(A) output on one complete residual-refined fibre. The norm is outside the full physical integral, and the four endpoint multipliers have already been evaluated.

Equations

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

theorem Anderson4D.R324PaperEndpointPhysicalBound.toQuadZeroShift {rho : SmoothCutoff} {K : ℝ} (h : R324PaperEndpointPhysicalBound rho K) : R324RefinedQuadZeroShiftBound rho K

Exact endpoint-factor cancellation turns Step 4(A) into the zero-shift quadruple-harvest input. No estimate is changed here; positivity of the two Green Fourier multipliers is the only ingredient.