The total-mass discharge of the R-324 residual slot budget

R324KeyedPrimitiveCollapse proves that the per-key interface R324KeyedCoreL1DecayBound is intrinsically ε-divergent: at m = 1 the grouped mass of the key k is a fixed positive multiple of ‖ρ̂(εk)‖², so a per-key eighth-order decay costs ε⁻¹⁶ per constant unit. This file abandons per-key decay entirely and bounds the total cost-weighted slot series by the exact fibre regrouping:

• the common-increment fibres partition the raw configurations, so the keyed slot series reassembles into the ungrouped raw mode series (tsumByKey fibration, no multiplicity loss);
• one reciprocal routed cost is dominated slotwise by the raw-mode bracket (key ∈ {0, q, -q}), and the raw series factorizes over the m frequency slots;
• each free slot pays the sharp scaled lattice mass ∑_k ‖ρ̂(εk)‖² ≲ ε⁻⁴ and the marked slot pays ∑_k ⟨k⟩⁸‖ρ̂(εk)‖² ≲ ε⁻¹², via the order-8 Schwartz bound and the block-decomposed scaled lattice sum ∑_{n∈ℤ}(1+δ|n|)⁻² ≤ 8/δ.

The resulting ledger is |log ε| · Σ ≤ E · U^m · ε^{-(4m+8)} · |log ε|, which yields R324SlotLogBudget ρ hm ε (A₁ ε⁻⁶): the slot-budget amplitude improves from the keyed ε⁻¹⁶ to ε⁻⁶ per constant unit. The power ε⁻⁶ is sharp for this norm-inside interface: at m = 1 the marked slot series is bounded below by a positive multiple of ∑_k ⟨k⟩⁸‖ρ̂(εk)‖² ≍ ε⁻¹² (the m = 1 identity of the keyed-collapse header), and the budget shape C^{2m}|log ε|^m forces C ≳ ε⁻⁶ there. The paper-scale amplitude (ε-uniform C) is therefore unreachable through R324SlotLogBudget as stated; this file delivers the strongest ε-power version, and the capstone instantiation carries the amplitude 64 · A₁ · ε⁻⁶.

One-dimensional lattice sums

Scaled one-dimensional lattice sums

Slotwise product factorization

The scaled lattice bracket sum on ℤ⁴

The order-8 covariance symbol bound

theorem Anderson4D.SmoothCutoff.exists_covarianceModeCoeff_order8_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {ε : ℝ}, 0 < ε → ∀ (k : Z4), ‖ρ.covarianceModeCoeff ε k‖ ≤ C * ((1 + ε / (2 * Real.pi) * ‖z4EuclideanFrequency k‖) ^ 16)⁻¹

Order-8 scaled symbol bound. Every covariance Fourier coefficient is dominated by C (1 + δ‖k‖)⁻¹⁶ with δ = ε/(2π) and an ε-uniform constant: the order-8 Schwartz bound, squared.

The total-mass slot weight

The slot modes of a raw refined configuration

The raw total slot mass

The exact fibre regrouping

The total-mass ledger

noncomputable def Anderson4D.r324TotalScheduleEnvelope (m : ℕ) : ℝ

Schedule envelope: total refined skeleton mass weighted by the contraction-fibre cardinalities. This ε-free constant is the same envelope that prices the proved keyed route.

Equations

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

theorem Anderson4D.r324TotalScheduleEnvelope_nonneg (m : ℕ) : 0 ≤ r324TotalScheduleEnvelope m

theorem Anderson4D.exists_tsum_groupedCoreL1_mul_cost_totalMass (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) : ∃ (U : ℝ), 0 < U ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (i : Fin m), ∑' (p : R324RefinedScheduleIndex m × ℕ), ρ.r324GroupedRefinedCoreL1 hm ε p * SmoothCutoff.r324GroupedIncrementCost hm p.2 i ≤ r324TotalScheduleEnvelope m * (U ^ m * ε⁻¹ ^ (4 * m + 8))

The sharp total-mass ledger. For every marked slot, the cost-weighted grouped slot series carries exactly ε^{-(4m+8)}: one ε⁻⁴ covariance mass per frequency slot and one extra ε⁻⁸ for the marked reciprocal cost. The constant U is ε-uniform and m-uniform; the envelope carries the schedule combinatorics. No |log ε| weight is consumed.

Discharge of the residual slot budget at amplitude ε⁻⁶

theorem Anderson4D.exists_r324SlotLogBudget_totalMass (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) : ∃ (A₁ : ℝ), 0 < A₁ ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → R324SlotLogBudget ρ hm ε (A₁ * ε⁻¹ ^ 6)

Total-mass discharge of the residual slot budget. The budget constant is A₁ ε⁻⁶ with A₁ uniform in ε: the ledger ε^{-(4m+8)} ≤ ε^{-12m} holds for every m ≥ 1 and is saturated at m = 1, where the marked slot series is a positive multiple of ∑_k ⟨k⟩⁸‖ρ̂(εk)‖² ≍ ε⁻¹². This improves the proved keyed amplitude 1024 A₀ ε⁻¹⁶ (exists_r324SlotLogBudget_final) to ε⁻⁶, the optimal power for the norm-inside interface.

Capstone instantiations at amplitude ε⁻⁶

theorem Anderson4D.exists_deterministicMoment_paper_bound_totalMass (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) : ∃ (outerConstant : ℝ) (A : ℝ), 0 < outerConstant ∧ 0 < A ∧ ∀ (lam : ℝ) (α β : Z4), 0 ≤ lam → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ paperDeterministicMomentRHS outerConstant (64 * (A * ε⁻¹ ^ 6)) lam ε m α β

The R-324 deterministic moment bound, total-mass form. Every analytic input is discharged; the slot budget is supplied by the total-mass ledger, so the amplitude carries ε⁻⁶ (improving the proved keyed capstone exists_deterministicMoment_paper_bound_final from ε⁻¹⁶). The power ε⁻⁶ is optimal for the norm-inside grouped interface (see the header); the paper-scale amplitude — A independent of ε — is not claimed.

theorem Anderson4D.exists_deterministicMoment_decay_bound_totalMass (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hlog : 1 ≤ |Real.log ε|) (hmtrunc : m ≤ truncOrder ε) : ∃ (outerConstant : ℝ) (A : ℝ), 0 < outerConstant ∧ 0 < A ∧ ∀ (lam : ℝ) (α β : Z4), 0 ≤ lam → ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ lamEps lam ε ^ 2 * outerConstant * (64 * (A * ε⁻¹ ^ 6) * lam) ^ (2 * m - 2) * paperDeterministicMomentDecay ε α β

Literal decay form of the total-mass estimate: the min bracket is bounded by the P-3.5b-det decay ε⁻⁸⟨α⟩⁻⁴⟨β⟩⁻⁴⟨ε²(α+β)⟩⁻⁸, at amplitude 64 A ε⁻⁶.