The two external-frequency cases in paper Step 4(B)

The first-large-factor selector is needed only when the conserved external shift α + β is nonzero. At zero shift the central paper bracket is exactly one, so the phase-free Steps 2--3 estimate is already the required bound.

This file contains only that case split. In particular, it introduces no routewise norm and no positive route-mass estimate.

The phase-free zero-shift boundary

def Anderson4D.R324RefinedQuadZeroShiftBound (ρ : SmoothCutoff) (K : ℝ) : Prop

The zero-shift instance of the paper quadruple-harvest estimate. Its right-hand side is exactly the paper-scale target with eighthOrderFrequencyDecay 0 = 1.

Equations

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

theorem Anderson4D.r324RefinedPostCollapsePaperQuadHarvestBound_of_open_and_zero {ρ : SmoothCutoff} {K : ℝ} (hopen : ρ.R324RefinedQuadOpenCovarianceSeriesBound K) (hzero : R324RefinedQuadZeroShiftBound ρ K) : R324RefinedPostCollapsePaperQuadHarvestBound ρ K

The paper-scale quadruple ledger follows by the literal two cases: nonzero conserved shift uses the first-large open covariance series, while zero shift uses the phase-free Steps 2--3 estimate.