The signed central-decay budget: low-frequency closure

This file closes the low central-frequency half of R324SignedCentralDecayBudget unconditionally from the interior inserted-majorant estimate (Statement 1), and isolates the exact high-frequency residue.

• eighthOrderFrequencyDecay_eps_scale_le — the paper's ε⁻⁸ endpoint sacrifice converts any eighth-order decay at covariance scale ε into the routed decay at every weaker scale, with no loss: (1+x²)⁴ ≤ ε⁻⁸ (1+(εy)²)⁴ for x ≤ y.
• norm_deterministicMomentPairingSum_le_modeDecay_mul_card_majorant — the schedule decomposition, the universal per-fibre mode decay 16⟨α⟩⁻⁴⟨β⟩⁻⁴, the interior estimate, and the count 16^{2m} give ‖Σ‖ ≤ ⟨α⟩⁻⁴⟨β⟩⁻⁴ · 16^{2m} · ∫ inserted majorant.
• signedCentralDecay_ineq_of_interiorCore_lowFrequency — for ‖freq(α+β)‖ ≤ ε⁻¹ the routed decay unit at one increment is worth ε⁸/16, so the ε⁻⁸ sacrifice closes the budget inequality.
• R324HighCentralFrequencySignedBound — the residue: the budget's own ∃ nInc ≤ truncOrder ε inequality, required only for ‖freq(α+β)‖ > ε⁻¹.
• exists_deterministicMoment_paper_bound_of_interiorCore_and_highFrequency and its literal decay-bracket corollary — the frozen (3.24) shape at the explicit ε-uniform outer constant 16·(Cball·sC² + 2·Creg)·(16 pC)², from Statement 1 plus the high-frequency residue alone.

The amplitude ledger is exact: aggregated mass 16·16^{2m}·∫maj ≤ 16·16^{2m}·(pC λ)^{2m}·CK/|log ε| = λ_ε² · [16·CK·(16 pC)²] · ((16 pC) λ)^{2m-2}, so the mode-decay route consumes the amplitude with no ε or log slack, and the ε⁻⁸ bracket is spent exactly once, on the passage from unit frequency to ε⁻¹.

theorem Anderson4D.one_add_sq_le_inv_sq_mul_one_add_eps_sq {ε y : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) : 1 + y ^ 2 ≤ ε⁻¹ ^ 2 * (1 + (ε * y) ^ 2)

One quadratic bracket at scale ε absorbs the unit-scale bracket at cost ε⁻².

theorem Anderson4D.eighthOrderFrequencyDecay_eps_scale_le {ε x y : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hx : 0 ≤ x) (hxy : x ≤ y) : eighthOrderFrequencyDecay (ε * y) ≤ ε⁻¹ ^ 8 * eighthOrderFrequencyDecay x

Scale conversion at the endpoint sacrifice. An eighth-order central decay at covariance scale ε dominates, after paying the paper's ε⁻⁸ endpoint loss, the same decay at any weaker scale x ≤ y; in particular at the routed increment scale y / nInc.

theorem Anderson4D.eps_pow_eight_div_sixteen_le_eighthOrderFrequencyDecay {ε y : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hy : 0 ≤ y) (hyε : y ≤ ε⁻¹) : ε ^ 8 / 16 ≤ eighthOrderFrequencyDecay y

Below the covariance frequency ε⁻¹, the eighth-order decay unit is worth at least ε⁸/16: the paper's endpoint sacrifice ε⁻⁸ buys the whole low-central-frequency regime.

theorem Anderson4D.norm_deterministicMomentPairingSum_le_modeDecay_mul_card_majorant {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {primitiveConstant supportConstant : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hm : 0 < m) (α β : Z4) (hcore : R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * (16 ^ (2 * m) * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure)

Mode-decay aggregation over the refined schedule set. The interior inserted-majorant estimate (Statement 1) turns the universal per-fibre mode decay into a bound on the full signed pairing sum by ⟨α⟩⁻⁴⟨β⟩⁻⁴ times 16^{2m} copies of the integrated majorant.

theorem Anderson4D.signedCentralDecay_ineq_of_interiorCore_lowFrequency {ρ : SmoothCutoff} {lam ε amplitude : ℝ} {m : ℕ} {primitiveConstant supportConstant : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hm : 0 < m) (α β : Z4) (hcore : R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant) (hAmaj : 16 * (16 ^ (2 * m) * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure) ≤ amplitude) (hlow : ‖z4EuclideanFrequency (α + β)‖ ≤ ε⁻¹) : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ amplitude * r324EndpointLoss ε α β * eighthOrderFrequencyDecay ((↑1)⁻¹ * ‖z4EuclideanFrequency (α + β)‖)

Low central-frequency branch of the signed budget. Below the covariance frequency ε⁻¹ the routed decay unit at one increment is worth ε⁸/16, so the mode-decay aggregation plus the paper's ε⁻⁸ endpoint sacrifice already deliver the routed inequality.

def Anderson4D.R324HighCentralFrequencySignedBound (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (amplitude : ℝ) : Prop

The precise residual oscillation statement in the high regime. Only central frequencies above the covariance scale ε⁻¹ remain: there the signed pairing sum must carry one eighth-order decay unit at unit lattice scale beyond the endpoint loss. The complementary regime ‖freq(α+β)‖ ≤ ε⁻¹ is discharged unconditionally by signedCentralDecay_ineq_of_interiorCore_lowFrequency, so this Prop is strictly smaller than R324SignedCentralDecayBudget.

Equations

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

theorem Anderson4D.r324SignedCentralDecayBudget_of_interiorCore_and_highFrequency {ρ : SmoothCutoff} {lam ε amplitude : ℝ} {m : ℕ} {primitiveConstant supportConstant : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hm : 0 < m) (hlog : 1 ≤ |Real.log ε|) (α β : Z4) (hcore : R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant) (hAmaj : 16 * (16 ^ (2 * m) * ∫ (z : T4), primitiveInsertedMajorant primitiveConstant lam ε supportConstant m z ∂paperMeasure) ≤ amplitude) (hhigh : R324HighCentralFrequencySignedBound ρ lam ε m amplitude) : R324SignedCentralDecayBudget ρ lam ε m α β amplitude

Statement 2 from Statement 1 and the high-frequency residue. The full signed central-decay budget follows, at one routed increment, from the interior inserted-majorant estimate (which covers all central frequencies up to ε⁻¹) together with the high-frequency signed bound.

theorem Anderson4D.lamEps_sq_eq (lam ε : ℝ) : lamEps lam ε ^ 2 = lam ^ 2 / |Real.log ε|

λ_ε² = λ²/|log ε|.

theorem Anderson4D.paper_amplitude_eq_majorant_budget (CK primitiveConstant lam ε : ℝ) {m : ℕ} (hm : 0 < m) : lamEps lam ε ^ 2 * (16 * CK * (16 * primitiveConstant) ^ 2) * (16 * primitiveConstant * lam) ^ (2 * m - 2) = 16 * (16 ^ (2 * m) * ((primitiveConstant * lam) ^ (2 * m) * (CK / |Real.log ε|)))

The paper-shaped amplitude at outerConstant = 16·CK·(16 pC)² matches the aggregated majorant budget exactly.

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_interiorCore_and_highFrequency {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 < m → 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant → R324HighCentralFrequencySignedBound ρ lam ε m (lamEps lam ε ^ 2 * outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2)) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (16 * primitiveConstant) lam ε m α β

The reduced final assembly. The paper bound (3.24), in its frozen paperDeterministicMomentRHS shape at an ε-uniform outer constant, follows from the interior inserted-majorant estimate (Statement 1) together with only the high-frequency residue of the signed central-decay budget: central frequencies ≤ ε⁻¹ are closed unconditionally here. The outer constant is explicit: 16·(Cball·sC² + 2·Creg)·(16 pC)² with Cball, Creg the universal majorant integration constants.

theorem Anderson4D.exists_deterministicMoment_decay_bound_of_interiorCore_and_highFrequency {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 < m → 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → R324InteriorCoreMajorantBound ρ lam ε m primitiveConstant supportConstant → R324HighCentralFrequencySignedBound ρ lam ε m (lamEps lam ε ^ 2 * outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2)) → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerConstant * (16 * primitiveConstant * lam) ^ (2 * m - 2) * paperDeterministicMomentDecay ε α β

Literal decay-bracket corollary of the reduced assembly: the min bracket is bounded by the explicit ε⁻⁸⟨α⟩⁻⁴⟨β⟩⁻⁴⟨ε²(α+β)⟩⁻⁸ decay of P-3.5b-det.

theorem Anderson4D.R324SignedCentralDecayBudget.mono {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} {amplitude amplitude' : ℝ} (h : R324SignedCentralDecayBudget ρ lam ε m α β amplitude) (hle : amplitude ≤ amplitude') : R324SignedCentralDecayBudget ρ lam ε m α β amplitude'

The signed central-decay budget is monotone in the amplitude.