The complementary low-frequency branch in R-324

At the selected central scale, the branch ε² L < 1 does not need a high-frequency restriction on the chosen Fourier mode. The cutoff symbol is bounded by one, the target eighth-order decay is bounded below by an absolute constant, and the two dummy chain edges cost at most O(ε⁻⁸) under the natural box bound M ≤ ε⁻¹.

This file contains only that scalar ledger and its one-open-edge primitive consumer.

Scalar low-frequency ledger

theorem Anderson4D.SmoothCutoff.one_div_sixteen_le_eighthOrderFrequencyDecay {x : ℝ} (hx : 0 ≤ x) (hxone : x < 1) : 1 / 16 ≤ eighthOrderFrequencyDecay x

On the central low-frequency branch, the target eighth-order decay has the uniform lower bound 1 / 16.

theorem Anderson4D.SmoothCutoff.norm_covarianceModeCoeff_le_whiteNoiseScaleSq (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ‖ρ.covarianceModeCoeff ε k‖ ≤ ‖↑NoiseModel.whiteNoiseFourierScale ^ 2‖

The covariance Fourier coefficient is uniformly bounded by the fixed white-noise half-density normalization.

theorem Anderson4D.SmoothCutoff.boxPenalty_sq_le_twentyfive_mul_epsInv_pow_eight {ε : ℝ} {M : ℕ} (hε : 0 < ε) (hεone : ε ≤ 1) (hM : ↑M ≤ ε⁻¹) : (1 + (2 * ↑M) ^ 2) ^ 2 ≤ 25 * ε⁻¹ ^ 8

The square box penalty is bounded by 25 ε⁻⁸. This deliberately uses the weaker eighth-order budget needed by the low-frequency branch; the elementary box estimate actually loses only four powers.

theorem Anderson4D.SmoothCutoff.exists_lowFrequency_boxPenalty_sq_mul_covarianceModeCoeff_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {ε L : ℝ} {M : ℕ} {k : Z4}, 0 < ε → ε ≤ 1 / 4 → 0 ≤ L → ε ^ 2 * L < 1 → ↑M ≤ ε⁻¹ → (1 + (2 * ↑M) ^ 2) ^ 2 * ‖ρ.covarianceModeCoeff ε k‖ ≤ C * ε⁻¹ ^ 8 * eighthOrderFrequencyDecay (ε ^ 2 * L)

Complete selected-mode scalar ledger on the complementary branch ε² L < 1. No membership assumption on k is present.

One-open-edge primitive consumer

theorem Anderson4D.SmoothCutoff.exists_selectedOpenEdgeLowFrequencyPrimitiveConsumer (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ {t : PlaneTree} {m M : ℕ} {κ : PartialPairing (Fin m)} {a b : Fin m} {w : Fin m → HeppLeaf t} {Nm : t.HeppMarking} {z : HeppLeaf t → Fin 4 → ℤ} {ε L : ℝ} {k : Z4}, 0 < m → κ a = b → a < b → κ.IsFull → IsPrimitive κ → (∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) → IsAdmissible Nm M z → 0 < ε → ε ≤ 1 / 4 → 0 ≤ L → ε ^ 2 * L < 1 → ↑M ≤ ε⁻¹ → NoProperLeafBlock (openEdgeAugmentedWord w a b) ∧ ‖ρ.covarianceModeCoeff ε k‖ * heppChainWeight z w ≤ C * ε⁻¹ ^ 8 * eighthOrderFrequencyDecay (ε ^ 2 * L) * heppChainWeight z (openEdgeAugmentedWord w a b)

The low-central-scale counterpart of the high-frequency one-open-edge consumer. The selected coefficient pays the two dummy chain edges at the explicit ε⁻⁸ cost, with no restriction on its Fourier mode.