Paper Step 4(B) only on the genuinely high central-frequency branch

Paper Section 4.2 invokes the projected-noise factor only when epsilon^2 * |alpha + beta| >= 1. On the complementary branch the central bracket is bounded below by 1 / 16, and the arbitrary-shift four-endpoint estimate already gives the desired bound. This file keeps that case split explicit, so the first-high physical producer is not asked to prove a statement outside the branch where the paper uses it.

Exact reassembly and the genuinely high branch

theorem Anderson4D.SmoothCutoff.r324RefinedPhysicalIntegral_eq_openCovarianceSeries (rho : SmoothCutoff) {epsilon : ℝ} (m : ℕ) (alpha beta : Z4) (hepsilon : 0 < epsilon) (hepsilonOne : epsilon ≤ 1) (hexternal : alpha + beta ≠ 0) (hm : 0 < m) (hmtrunc : m ≤ truncOrder epsilon) (p : R324RefinedScheduleIndex m) : r324RefinedPhysicalIntegral rho epsilon m alpha beta p = rho.r324RefinedQuadOpenCovarianceSeries hm epsilon alpha beta hexternal hepsilon hepsilonOne hmtrunc p

Away from zero conserved shift, the open-covariance series is exactly the original refined physical integral. This is only a rebracketing of the two exact identities already used in the covariance reassembly; in particular, no modulus enters here.

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

The fixed-slot physical producer on the large-central-frequency branch. The complete slot source remains signed until the displayed norm.

Equations

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

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

Numerical form of the high-branch fixed-slot estimate.

Equations

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

theorem Anderson4D.SmoothCutoff.R324PaperHighSlotWeightedMajorantBound.toHighSlotCollapseBound {rho : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (h : rho.R324PaperHighSlotWeightedMajorantBound primitiveConstant supportConstant) : ∃ (K : ℝ), 0 < K ∧ rho.R324RefinedQuadHighOperatorSlotCollapseBound K

The common inserted-majorant calculation closes the high-slot scalar ledger; the extra high-branch premise is simply passed to the producer.

theorem Anderson4D.SmoothCutoff.R324RefinedQuadHighOperatorSlotCollapseBound.openSeries_of_high {rho : SmoothCutoff} {K : ℝ} (hK : 0 ≤ K) (h : rho.R324RefinedQuadHighOperatorSlotCollapseBound K) {epsilon : ℝ} (m : ℕ) (alpha beta : Z4) (hepsilon : 0 < epsilon) (hepsilonSmall : epsilon ≤ 1 / 4) (hlog : 1 ≤ |Real.log epsilon|) (hm2 : 2 ≤ m) (hmtrunc : m ≤ truncOrder epsilon) (hexternal : alpha + beta ≠ 0) (hm : 0 < m) (p : R324RefinedScheduleIndex m) : 1 ≤ epsilon ^ 2 * ‖z4EuclideanFrequency (alpha + beta)‖ → ‖rho.r324RefinedQuadOpenCovarianceSeries hm epsilon alpha beta hexternal hepsilon ⋯ hmtrunc p‖ ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (↑m ^ 8 * (2 * K) ^ m * |Real.log epsilon| ^ (m - 1) * epsilon⁻¹ ^ 8 * eighthOrderFrequencyDecay (epsilon ^ 2 * ‖z4EuclideanFrequency (alpha + beta)‖))

On the branch on which the paper invokes the first-high selector, the single-slot estimate closes the complete signed open series. The only triangle inequality is the finite sum over at most m possible slots; m <= 2^m is absorbed into the geometric base.

Literal Step 4(A)/Step 4(B) case split

theorem Anderson4D.SmoothCutoff.R324PaperEndpointAllShiftPhysicalBound.openSeries_of_highSlot {rho : SmoothCutoff} {K0 K1 : ℝ} (hK0 : 0 ≤ K0) (hK1 : 0 ≤ K1) (hEndpoint : R324PaperEndpointAllShiftPhysicalBound rho K0) (hHigh : rho.R324RefinedQuadHighOperatorSlotCollapseBound K1) : rho.R324RefinedQuadOpenCovarianceSeriesBound (max (16 * max 1 K0) (2 * K1))

Paper Step 4 closes the open covariance series by the literal central frequency split. If epsilon^2 * |alpha + beta| < 1, the arbitrary-shift four-endpoint estimate supplies the whole series and the target central decay costs only the absolute factor 16. Otherwise the first-high slot estimate applies and the finite slot count costs 2^m.

Step 4 capstone

theorem Anderson4D.exists_r324PaperPostCollapseBracket_of_endpoint_and_highSlot {rho : SmoothCutoff} {endpointPrimitive endpointSupport highPrimitive highSupport : ℝ} (hEndpointPrimitive : 0 < endpointPrimitive) (hEndpointSupport : 0 < endpointSupport) (hHighPrimitive : 0 < highPrimitive) (hHighSupport : 0 < highSupport) (hEndpoint : R324PaperEndpointAllShiftWeightedMajorantBound rho endpointPrimitive endpointSupport) (hHigh : rho.R324PaperHighSlotWeightedMajorantBound highPrimitive highSupport) : ∃ (K : ℝ), 0 ≤ K ∧ R324RefinedPostCollapsePaperBracketBound rho K

The two literal Step 4 outputs, assembled only as far as the post-collapse paper bracket. This is the deterministic seam shared by P-3.5b-det and the later conditional-main assembly.

theorem Anderson4D.r324PaperScale_hdet_of_endpoint_and_highSlot (rho : SmoothCutoff) {endpointPrimitive endpointSupport highPrimitive highSupport : ℝ} (hEndpointPrimitive : 0 < endpointPrimitive) (hEndpointSupport : 0 < endpointSupport) (hHighPrimitive : 0 < highPrimitive) (hHighSupport : 0 < highSupport) (hEndpoint : R324PaperEndpointAllShiftWeightedMajorantBound rho endpointPrimitive endpointSupport) (hHigh : rho.R324PaperHighSlotWeightedMajorantBound highPrimitive highSupport) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 < lam → ∀ᶠ (epsilon : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder epsilon → ∀ (alpha beta : Z4), ‖deterministicMomentPairingSum rho lam epsilon m alpha beta‖ ≤ paperDeterministicMomentRHS outerC powerC lam epsilon m alpha beta

P-3.5b-det from the two paper Step 4 outputs. The signed Steps 2--3 reduction is supplied by its unconditional producer, and the conclusion is the eventually-small-scale deterministic pairing-sum bound with the exact paper central-frequency decay.

theorem Anderson4D.mainConditional_of_paperAllShiftEndpoint_and_highSlot {M : NoiseModel} {rho : SmoothCutoff} {endpointPrimitive endpointSupport highPrimitive highSupport : ℝ} (hEndpointPrimitive : 0 < endpointPrimitive) (hEndpointSupport : 0 < endpointSupport) (hHighPrimitive : 0 < highPrimitive) (hHighSupport : 0 < highSupport) (hEndpoint : R324PaperEndpointAllShiftWeightedMajorantBound rho endpointPrimitive endpointSupport) (hHigh : rho.R324PaperHighSlotWeightedMajorantBound highPrimitive highSupport) : MainConditional M rho

The two literal paper Step 4 producers close the conditional main theorem. The endpoint producer also supplies the zero conserved-shift branch; on the nonzero branch the preceding low/high split supplies the complete open covariance-series estimate.

theorem Anderson4D.mainConditional_of_paperEndpointCases_and_highSlot {M : NoiseModel} {rho : SmoothCutoff} {endpointPrimitive endpointSupport highPrimitive highSupport : ℝ} (hEndpointPrimitive : 0 < endpointPrimitive) (hEndpointSupport : 0 < endpointSupport) (hHighPrimitive : 0 < highPrimitive) (hHighSupport : 0 < highSupport) (hResidual : R324PaperResidualEndpointWeightedMajorantBound rho endpointPrimitive endpointSupport) (hFull : R324PaperFullEndpointWeightedMajorantBound rho endpointPrimitive endpointSupport) (hHigh : rho.R324PaperHighSlotWeightedMajorantBound highPrimitive highSupport) : MainConditional M rho

Final producer-facing form: the residual endpoint carrier, the full/full endpoint carrier, and the genuinely-high selected-slot carrier are the only remaining physical inputs.

theorem Anderson4D.r324PaperScale_hdet_of_exists_paperEndpointCases_and_highSlot (rho : SmoothCutoff) (hResidual : ∃ (residualConstant : ℝ) (supportConstant : ℝ), 0 < residualConstant ∧ 0 < supportConstant ∧ R324PaperResidualEndpointWeightedMajorantBound rho residualConstant supportConstant) (hFull : ∀ {supportConstant : ℝ}, 0 < supportConstant → ∃ (fullConstant : ℝ), 0 < fullConstant ∧ R324PaperFullEndpointZeroShiftWeightedMajorantBound rho fullConstant supportConstant) (hHigh : ∃ (highConstant : ℝ) (highSupport : ℝ), 0 < highConstant ∧ 0 < highSupport ∧ rho.R324PaperHighSlotWeightedMajorantBound highConstant highSupport) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 < lam → ∀ᶠ (epsilon : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder epsilon → ∀ (alpha beta : Z4), ‖deterministicMomentPairingSum rho lam epsilon m alpha beta‖ ≤ paperDeterministicMomentRHS outerC powerC lam epsilon m alpha beta

Existential producer-facing P-3.5b-det. The two endpoint branches may choose independent primitive constants, exactly as in the final conditional-main wrapper below.

theorem Anderson4D.mainConditional_of_exists_paperEndpointCases_and_highSlot {M : NoiseModel} {rho : SmoothCutoff} (hResidual : ∃ (residualConstant : ℝ) (supportConstant : ℝ), 0 < residualConstant ∧ 0 < supportConstant ∧ R324PaperResidualEndpointWeightedMajorantBound rho residualConstant supportConstant) (hFull : ∀ {supportConstant : ℝ}, 0 < supportConstant → ∃ (fullConstant : ℝ), 0 < fullConstant ∧ R324PaperFullEndpointZeroShiftWeightedMajorantBound rho fullConstant supportConstant) (hHigh : ∃ (highConstant : ℝ) (highSupport : ℝ), 0 < highConstant ∧ 0 < highSupport ∧ rho.R324PaperHighSlotWeightedMajorantBound highConstant highSupport) : MainConditional M rho

Final existential producer interface. The residual and full/full endpoint proofs may choose independent primitive constants; the full/full producer only has to work at the support radius selected by the residual proof. The high-slot proof remains completely independent.