Keyed primitive collapse for the R-324 grouped interior cores

This file proves the residual keyed interior bound R324KeyedCoreL1DecayBound at an explicit ε-dependent amplitude A₀ · ε⁻¹⁶, and instantiates the capstone exists_deterministicMoment_paper_bound_of_keyedDecay accordingly.

The mechanism

For one common-increment group (p, b) the interior L¹ mass is bounded by the proved skeleton/covariance separation, and the two eighth-order decay units per frequency slot are extracted from the covariance weight itself:

• every slot of a raw configuration in the fibre of the key b carries a mode qᵢ with increment key keyᵢ ∈ {0, qᵢ, -qᵢ}, so slotwise ⟨qᵢ⟩⁻⁸ ≤ ⟨keyᵢ⟩⁻⁸ (r324KeyedSlotDecay_le_keyDecay);
• the cutoff symbol obeys the arbitrary-order Schwartz bound, which at order 16 yields the slotwise majorant ‖covarianceModeCoeff ε k‖ ≤ B ε⁻³² ⟨k⟩⁻³² (exists_covarianceModeCoeff_keyedDecay_bound); two of the four eighth-order units are retained against the key, the remaining two pay the free-mode lattice sums (≤ 4096 per slot).

Why the amplitude carries ε⁻¹⁶

The prefactor ε⁻¹⁶ is intrinsic to the interface, not an artifact: r324GroupedRefinedCoreL1 integrates the pointwise norm of the grouped core, and every Fourier character has modulus one, so no physical oscillation survives inside this quantity. Already at m = 1 the interior skeleton is an empty product and the grouped mass of the key k equals a fixed positive multiple of ‖ρ̂(εk)‖²; since ‖ρ̂(εk)‖ ≈ ‖ρ̂(0)‖ for ‖k‖ ≲ ε⁻¹, no ε-uniform constant A can satisfy ‖ρ̂(εk)‖² ≤ A² ⟨k⟩⁻¹⁶ on that range. An ε-uniform keyed bound would therefore require keeping the endpoint/interior oscillations outside the norm, i.e. a different interface than R324KeyedCoreL1DecayBound. The optimal rate through this interface is A ≍ ε⁻⁸; the constant obtained here is A₀ ε⁻¹⁶ because the free-mode lattice sums are paid by the same slotwise symbol bound.

The slotwise keyed symbol bound

theorem Anderson4D.SmoothCutoff.exists_covarianceModeCoeff_keyedDecay_bound (ρ : SmoothCutoff) : ∃ (B : ℝ), 0 < B ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (k : Z4), ‖ρ.covarianceModeCoeff ε k‖ ≤ B * ε⁻¹ ^ 32 * eighthOrderFrequencyDecay ‖z4EuclideanFrequency k‖ ^ 4

Slotwise keyed symbol bound. Every covariance Fourier coefficient carries four eighth-order decay units at the cost of ε⁻³²: ‖covarianceModeCoeff ε k‖ ≤ B ε⁻³² ⟨k⟩⁻³². This is the order-16 Schwartz bound for the fixed smooth cutoff.

The slot modes of a raw refined configuration

Lattice sums of the keyed decay weight

The keyed covariance-weight collapse

The keyed interior collapse

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

The keyed interior bound at explicit ε-dependent amplitude. For every cutoff and truncation order there is a constant A₀ with R324KeyedCoreL1DecayBound ρ hm ε (A₀ ε⁻¹⁶) throughout the capstone range: the grouped interior L¹ mass of one common-increment group carries two eighth-order decay units per frequency slot at amplitude (A₀ ε⁻¹⁶)^{2m} |log ε|^{m-1}.

Unconditional capstone instantiations

theorem Anderson4D.exists_deterministicMoment_paper_bound_final (ρ : 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 (65536 * A) lam ε m α β

The R-324 deterministic moment bound, unconditional form. Every analytic input is discharged; the keyed interior bound is supplied by exists_r324KeyedCoreL1DecayBound, so the amplitude carries the explicit factor ε⁻¹⁶ (see the header for why this factor is intrinsic to the L¹-keyed interface). The paper-scale amplitude — A independent of ε — is not claimed.

theorem Anderson4D.exists_deterministicMoment_decay_bound_final (ρ : 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 * (65536 * A * lam) ^ (2 * m - 2) * paperDeterministicMomentDecay ε α β

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

theorem Anderson4D.exists_r324SlotLogBudget_final (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) : ∃ (A₀ : ℝ), 0 < A₀ ∧ R324SlotLogBudget ρ hm ε (1024 * (A₀ * ε⁻¹ ^ 16))

The residual slot budget holds unconditionally at the explicit ε-dependent primitive constant 1024 A₀ ε⁻¹⁶.