Paper Step 4 capstone

The zero conserved shift is supplied by the four-endpoint collapse of Step 4(A). A nonzero shift is supplied by the first-large-factor fixed-slot collapse of Step 4(B). This file only enlarges their geometric constants, performs the literal two-case split already recorded by the paper-scale quadruple-harvest API, and connects the result to the unconditional Steps 2--3 closure.

No physical integral is split and no modulus is moved in this file.

theorem Anderson4D.R324RefinedQuadZeroShiftBound.mono {rho : SmoothCutoff} {K0 K : ℝ} (hK0 : 0 ≤ K0) (hK : K0 ≤ K) (h : R324RefinedQuadZeroShiftBound rho K0) : R324RefinedQuadZeroShiftBound rho K

A zero-shift bound is monotone in its nonnegative geometric base.

theorem Anderson4D.SmoothCutoff.R324RefinedQuadOpenCovarianceSeriesBound.mono {rho : SmoothCutoff} {K0 K : ℝ} (hK0 : 0 ≤ K0) (hK : K0 ≤ K) (h : rho.R324RefinedQuadOpenCovarianceSeriesBound K0) : rho.R324RefinedQuadOpenCovarianceSeriesBound K

The complete open covariance-series bound is monotone in its nonnegative geometric base.

theorem Anderson4D.mainConditional_of_paperEndpoint_and_fixedSlot {M : NoiseModel} {rho : SmoothCutoff} (hEndpoint : ∃ (K0 : ℝ), 0 ≤ K0 ∧ R324PaperEndpointPhysicalBound rho K0) (hFixedSlot : ∃ (K1 : ℝ), 0 ≤ K1 ∧ rho.R324RefinedQuadOperatorSlotCollapseBound K1) : MainConditional M rho

Once the two paper Step 4 producers exist, the conditional main theorem follows with no further analytic hypothesis. Steps 2--3 are supplied by exists_r324PaperRefinedStep23Input; the Gabriel--Rosati input remains explicit inside MainConditional.