Conditional main theorem at the exact paper scale

Paper: R-324 — §4.2, (3.24) and conditional Theorem 1.1

This is the final assembly for the residual-refined route. Its routed input is R324RefinedPostCollapsePaperBracketBound, with the exact ⟨ε²(α+β)⟩⁻⁸ decay proved in Step 4(B). No stronger intermediate central-frequency estimate is assumed.

theorem Anderson4D.r324PaperScale_exists_deterministicMoment_paper_bound (ρ : SmoothCutoff) {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (hstep23 : R324PaperRefinedStep23Input ρ primitiveConstant supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324RefinedPostCollapsePaperBracketBound ρ K) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 ≤ lam → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerC powerC lam ε m α β

The fixed-scale deterministic estimate (3.24) from the paper's post-removal uniform bound and its exact ε² routed bound.

theorem Anderson4D.paperDeterministicMomentRHS_le_deterministicMomentRHS {outerC powerC lam ε : ℝ} {m : ℕ} {alpha beta : Z4} (houter : 0 ≤ outerC) (hpower : 0 ≤ powerC) (hlam : 0 ≤ lam) : paperDeterministicMomentRHS outerC powerC lam ε m alpha beta ≤ deterministicMomentRHS outerC powerC lam ε m alpha beta

The exact paper RHS is stronger than the sup-norm RHS whenever the named constants and coupling are nonnegative.

theorem Anderson4D.r324PaperScale_exists_deterministicMoment_bound (ρ : SmoothCutoff) {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (hstep23 : R324PaperRefinedStep23Input ρ primitiveConstant supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324RefinedPostCollapsePaperBracketBound ρ K) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 ≤ lam → ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (alpha beta : Z4), ‖deterministicMomentPairingSum ρ lam ε m alpha beta‖ ≤ deterministicMomentRHS outerC powerC lam ε m alpha beta

Compatibility form of the fixed-scale estimate for the downstream probability layer, obtained by forgetting only the stronger Euclidean Japanese bracket in the paper RHS.

theorem Anderson4D.r324PaperScale_hdet_paper (ρ : SmoothCutoff) {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (hstep23 : R324PaperRefinedStep23Input ρ primitiveConstant supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324RefinedPostCollapsePaperBracketBound ρ K) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 < lam → ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (alpha beta : Z4), ‖deterministicMomentPairingSum ρ lam ε m alpha beta‖ ≤ paperDeterministicMomentRHS outerC powerC lam ε m alpha beta

Eventually-small-scale P-3.5b-det with the exact Euclidean Japanese bracket printed in (3.24).

theorem Anderson4D.r324PaperScale_hdet (ρ : SmoothCutoff) {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (hstep23 : R324PaperRefinedStep23Input ρ primitiveConstant supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324RefinedPostCollapsePaperBracketBound ρ K) : ∃ (outerC : ℝ) (powerC : ℝ), 0 < outerC ∧ 0 < powerC ∧ ∀ (lam : ℝ), 0 < lam → ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ (m : ℕ), 1 ≤ m → m ≤ truncOrder ε → ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerC powerC lam ε m α β

The eventually-small-scale deterministic hypothesis at the exact paper central-frequency scale.

theorem Anderson4D.mainConditional_of_paperRefinedStep23_and_paperBracket {M : NoiseModel} {ρ : SmoothCutoff} {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) (hstep23 : R324PaperRefinedStep23Input ρ primitiveConstant supportConstant) (hbracket : ∃ (K : ℝ), 0 ≤ K ∧ R324RefinedPostCollapsePaperBracketBound ρ K) : MainConditional M ρ

Conditional Theorem 1.1 from the two paper-faithful §4.2 outputs. The Gabriel--Rosati input remains explicit in MainConditional.