Paper Step 4(B) at the complete signed-series boundary

Paper: R-324 — §4.2 Step 4(B), complete signed-series boundary

The paper obtains the central-frequency gain before splitting the complete operator expansion into selected slots. This module records the corresponding consumer interface: one norm is taken only after the complete signed open covariance series has been reassembled. It deliberately does not pass through the per-slot interface, whose triangle inequality is too early for the common-translation proof.

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

The paper Step 4(B) producer at the complete signed-series boundary.

Equations

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

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

Numerical high-branch estimate for the complete signed series.

Equations

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

theorem Anderson4D.SmoothCutoff.R324PaperHighWholeSeriesWeightedMajorantBound.toHighWholeSeriesCollapseBound {rho : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (h : rho.R324PaperHighWholeSeriesWeightedMajorantBound primitiveConstant supportConstant) : ∃ (K : ℝ), 0 < K ∧ rho.R324RefinedQuadHighWholeSeriesCollapseBound K

The common inserted-majorant calculation closes the whole-series scalar ledger without an additional slot-count triangle inequality.

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

Literal low/high central-frequency split using a whole-series high estimate. The low branch is unchanged from Step 4(A).

Conditional main-theorem capstone with the whole-series producer

theorem Anderson4D.exists_r324PaperPostCollapseBracket_of_endpoint_and_highWholeSeries {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.R324PaperHighWholeSeriesWeightedMajorantBound highPrimitive highSupport) : ∃ (K : ℝ), 0 ≤ K ∧ R324RefinedPostCollapsePaperBracketBound rho K

theorem Anderson4D.r324PaperScale_hdet_of_exists_paperEndpointCases_and_highWholeSeries (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.R324PaperHighWholeSeriesWeightedMajorantBound 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 P-3.5b-det interface using the complete-series high producer.

theorem Anderson4D.mainConditional_of_exists_paperEndpointCases_and_highWholeSeries {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.R324PaperHighWholeSeriesWeightedMajorantBound highConstant highSupport) : MainConditional M rho

Final conditional-main interface using the complete-series high producer.