The keyed-decay ledger for the R-324 slot budget

This file quantifies every structural ingredient of the residual slot budget R324SlotLogBudget:

• an explicit bound ∑_{k ∈ ℤ⁴} ⟨k⟩⁻⁸ ≤ 4096 for the eighth-order frequency decay (tsum_eighthOrderFrequencyDecay_z4_le);
• the exact slotwise product factorization of key sums over Fin m → ℤ⁴ (tsum_realSlotProduct);
• the exponential schedule count card (R324RefinedScheduleIndex m) ≤ 16 ^ (2m);
• the resulting discharge of the residual slot budget from a single per-key interior bound (r324SlotLogBudget_of_keyedCoreL1DecayBound), and the corresponding instantiations of the capstone.

The analytic estimate is isolated in the Prop R324KeyedCoreL1DecayBound: the grouped interior L¹ mass of one common-increment group must carry two eighth-order decay units per frequency slot, at the amplitude A^{2m} |log ε|^{m-1}. This is the iterated Proposition 4.1 estimate with keyed Fourier decay; the coarse proved majorant (r324GroupedRefinedCoreL1_le_skeleton_mul_covariance) is ε-divergent and cannot supply it.

Explicit one-dimensional lattice sums

Slotwise product factorization of key sums

The explicit eighth-order lattice budget on ℤ⁴

theorem Anderson4D.tsum_latticeSummabilityWeight_le : ∑' (k : Z4), latticeSummabilityWeight k ≤ 256

Explicit total mass of the product summability weight: ∑_{k ∈ ℤ⁴} ∏ᵢ (|kᵢ|+1)⁻² ≤ 256.

theorem Anderson4D.eighthOrderFrequencyDecay_le_latticeWeight (k : Z4) : eighthOrderFrequencyDecay ‖z4EuclideanFrequency k‖ ≤ 16 * latticeSummabilityWeight k

Pointwise comparison of the paper's ⟨k⟩⁻⁸ on the lattice with the product summability weight.

theorem Anderson4D.summable_eighthOrderFrequencyDecay_z4 : Summable fun (k : Z4) => eighthOrderFrequencyDecay ‖z4EuclideanFrequency k‖

The paper's ⟨k⟩⁻⁸ is summable on ℤ⁴.

theorem Anderson4D.tsum_eighthOrderFrequencyDecay_z4_le : ∑' (k : Z4), eighthOrderFrequencyDecay ‖z4EuclideanFrequency k‖ ≤ 4096

Explicit eighth-order lattice budget: ∑_{k ∈ ℤ⁴} (1+‖k‖²)⁻⁴ ≤ 4096.

The exponential schedule count

theorem Anderson4D.card_r324RefinedScheduleIndex_le (m : ℕ) : Fintype.card (R324RefinedScheduleIndex m) ≤ 16 ^ (2 * m)

The residual-refined schedule index is at most exponentially large: both layers are signatures, i.e. pairs of subsets of Fin (2m).

The keyed decay weight and the residual hypothesis

theorem Anderson4D.eighthOrderFrequencyDecay_le_one (x : ℝ) : eighthOrderFrequencyDecay x ≤ 1

The eighth-order decay never exceeds one.

noncomputable def Anderson4D.r324KeyedDecaySquared {m : ℕ} (hm : 0 < m) (b : ℕ) : ℝ

Two eighth-order decay units at every frequency slot of one common increment key.

Equations

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

theorem Anderson4D.r324KeyedDecaySquared_nonneg {m : ℕ} (hm : 0 < m) (b : ℕ) : 0 ≤ r324KeyedDecaySquared hm b

def Anderson4D.R324KeyedCoreL1DecayBound (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε A : ℝ) : Prop

The residual keyed interior bound. The grouped interior L¹ mass of one common-increment group carries the amplitude A^{2m} |log ε|^{m-1} and two eighth-order decay units per frequency slot. This is the quantitative iterated-Proposition-4.1 content with keyed Fourier decay; everything else in the slot budget is discharged unconditionally below.

Equations

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

The keyed slot sum

theorem Anderson4D.summable_keyedDecaySquared_mul_cost {m : ℕ} (hm : 0 < m) (i : Fin m) : Summable fun (b : ℕ) => r324KeyedDecaySquared hm b * SmoothCutoff.r324GroupedIncrementCost hm b i

The keyed slot series is summable.

theorem Anderson4D.tsum_keyedDecaySquared_mul_cost_le {m : ℕ} (hm : 0 < m) (i : Fin m) : ∑' (b : ℕ), r324KeyedDecaySquared hm b * SmoothCutoff.r324GroupedIncrementCost hm b i ≤ 4096 ^ m

The keyed slot budget: the complete keyed slot series is at most 4096^m.

Discharge of the residual slot budget

theorem Anderson4D.r324SlotLogBudget_of_keyedCoreL1DecayBound (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε A : ℝ} (hε : 0 < ε) (hlog : 1 ≤ |Real.log ε|) (hA : 0 ≤ A) (hkeyed : R324KeyedCoreL1DecayBound ρ hm ε A) : R324SlotLogBudget ρ hm ε (1024 * A)

The keyed interior bound discharges the residual slot budget. The schedule count pays 16^{2m}, the keyed slot sums pay 4096^m = 64^{2m}, and the marked |log ε| closes |log ε|^{m-1} to |log ε|^m; the budget constant is 1024·A.

Capstone instantiations

theorem Anderson4D.exists_deterministicMoment_paper_bound_of_keyedDecay {A : ℝ} (hA : 0 < A) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → R324KeyedCoreL1DecayBound ρ hm ε A → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (65536 * A) lam ε m α β

The R-324 deterministic moment paper bound from the keyed interior bound alone. Every ingredient of the slot budget other than R324KeyedCoreL1DecayBound — the schedule count, the keyed slot sums, the |log ε| ledger, the interior-core comparison, and the full majorant assembly — is discharged unconditionally.

theorem Anderson4D.exists_deterministicMoment_decay_bound_of_keyedDecay {A : ℝ} (hA : 0 < A) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4), 0 ≤ lam → 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → R324KeyedCoreL1DecayBound ρ hm ε A → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerConstant * (65536 * A * lam) ^ (2 * m - 2) * paperDeterministicMomentDecay ε α β

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