Discharging the routed window ledgers at low order

This file proves the two routed-branch Props of R324RoutedWindowBudget at the orders where they are true and reachable from the proved route-weight layer:

• exists_r324RoutedPerTermWindowBound_one — the nonzero-shift routed per-term ledger at m = 1. Endpoint-licensed zero deletion forces the single increment key of every surviving route to be exactly α + β; the marked slot cost ⟨α+β⟩⁸ against the symbol square at that same frequency is worth C·ε⁻⁸ pointwise, so the whole ledger collapses to finitely many contraction/selector labels at the windowed value C·ε⁻⁸ with no logarithm spent.
• exists_r324RoutedZeroShiftWindowBound_one and …_two — the zero-shift grouped ledger at m ≤ 2. The grouped weights carry no slot cost, so the raw covariance mass (C·ε⁻⁴)^m already fits under the windowed value C^m·L^{m-1}·ε⁻⁸ exactly for m ≤ 2.

The two ingredients proved here and reused by both branches are the pointwise marked-window bound ⟨k⟩⁸·‖ρ̂(εk)‖² ≤ C·ε⁻⁸ (from degree-six symbol decay) and the scaled symbol mass Σ_k ‖ρ̂(εk)‖² ≤ C·ε⁻⁴.

theorem Anderson4D.z4EuclideanFrequency_injective : Function.Injective z4EuclideanFrequency

The lattice-to-Euclidean frequency map is injective, so frequency conservation pins lattice keys exactly.

theorem Anderson4D.r324RoutedEval_pointwise_marked_bound (ρ : SmoothCutoff) : ∃ (CP : ℝ), 0 < CP ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (k : Z4), (1 + ‖z4EuclideanFrequency k‖ ^ 2) ^ 4 * ‖ρ.symbol ε k‖ ^ 2 ≤ CP * ε⁻¹ ^ 8

Pointwise marked window. One degree-eight slot cost against the symbol square at the same frequency is worth the endpoint sacrifice ε⁻⁸ at every single lattice mode.

theorem Anderson4D.r324RoutedEval_symbol_mass_le (ρ : SmoothCutoff) : ∃ (CS : ℝ), 0 < CS ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → (Summable fun (k : Z4) => ‖ρ.symbol ε k‖ ^ 2) ∧ ∑' (k : Z4), ‖ρ.symbol ε k‖ ^ 2 ≤ CS * ε⁻¹ ^ 4

Scaled symbol mass. The complete symbol-square lattice mass is one mollifier volume ε⁻⁴.

theorem Anderson4D.r324RoutedEval_norm_covarianceModeCoeff (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ‖ρ.covarianceModeCoeff ε k‖ = NoiseModel.whiteNoiseFourierScale ^ 2 * ‖ρ.symbol ε k‖ ^ 2

Exact norm of one covariance Fourier coefficient.

theorem Anderson4D.r324RoutedEval_covarianceMass_le (ρ : SmoothCutoff) : ∃ (CV : ℝ), 0 < CV ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∑' (k : Z4), ‖ρ.covarianceModeCoeff ε k‖ ≤ CV * ε⁻¹ ^ 4

Covariance coefficient mass. The total covariance Fourier mass is one mollifier volume ε⁻⁴.

theorem Anderson4D.r324RoutedEval_pointwise_coeff_bound (ρ : SmoothCutoff) : ∃ (CB : ℝ), 0 < CB ∧ ∀ {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (k : Z4), (1 + ‖z4EuclideanFrequency k‖ ^ 2) ^ 4 * ‖ρ.covarianceModeCoeff ε k‖ ≤ CB * ε⁻¹ ^ 8

Pointwise covariance-coefficient marked bound: one degree-eight slot cost against the coefficient at the same frequency is worth C·ε⁻⁸.

noncomputable def Anderson4D.SmoothCutoff.r324RoutedEvalSlotMode {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) (a : ℕ) : Fin m → Z4

The standard slot modes of one raw refined configuration.

Equations

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

theorem Anderson4D.SmoothCutoff.r324RoutedEval_covWeight_eq_prod (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (ε : ℝ) (p : R324RefinedScheduleIndex m) (a : ℕ) : ρ.r324RefinedRawCovarianceWeight hm ε p a = ∏ i : Fin m, ‖ρ.covarianceModeCoeff ε (r324RoutedEvalSlotMode hm p a i)‖

The raw covariance weight is the slotwise product of coefficient norms at the standard slot modes.

theorem Anderson4D.SmoothCutoff.r324RoutedEval_incrementKey_cases {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) (a : ℕ) (i : Fin m) : r324RefinedRawIncrementKey hm p a i = 0 ∨ r324RefinedRawIncrementKey hm p a i = r324RoutedEvalSlotMode hm p a i ∨ r324RefinedRawIncrementKey hm p a i = -r324RoutedEvalSlotMode hm p a i

The increment key of one slot is the slot mode, its negative, or zero.

theorem Anderson4D.SmoothCutoff.r324RoutedEval_keyCost_le_modeCost {m : ℕ} (hm : 0 < m) (p : R324RefinedScheduleIndex m) (a : ℕ) (i : Fin m) : (1 + ‖z4EuclideanFrequency (r324RefinedRawIncrementKey hm p a i)‖ ^ 2) ^ 4 ≤ (1 + ‖z4EuclideanFrequency (r324RoutedEvalSlotMode hm p a i)‖ ^ 2) ^ 4

The routed cost of one increment key never exceeds the cost of its slot mode.

theorem Anderson4D.r324RoutedEval_tsum_pi_prod_le_pow {F : Z4 → ℝ} (hF0 : ∀ (k : Z4), 0 ≤ F k) (hFs : Summable F) {M : ℝ} (hFM : ∑' (k : Z4), F k ≤ M) {m : ℕ} (hm : 0 < m) (hm2 : m ≤ 2) : (Summable fun (q : Fin m → Z4) => ∏ i : Fin m, F (q i)) ∧ ∑' (q : Fin m → Z4), ∏ i : Fin m, F (q i) ≤ M ^ m

Low-order product mass: at m ≤ 2 the assignment series of a slotwise product is bounded by the per-slot mass to the m-th power.

theorem Anderson4D.SmoothCutoff.r324RoutedEval_tsum_rawCovWeight_le (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (hm2 : m ≤ 2) {ε M : ℝ} (hε : 0 < ε) (hMass : ∑' (k : Z4), ‖ρ.covarianceModeCoeff ε k‖ ≤ M) (p : R324RefinedScheduleIndex m) : ∑' (a : ℕ), ρ.r324RefinedRawCovarianceWeight hm ε p a ≤ ↑(Nat.card (R324RefinedContractionIndex p)) * M ^ m

The complete raw covariance mass of one refined schedule at m ≤ 2: the contraction fibre pays its cardinality and each slot pays the full per-slot coefficient mass.

theorem Anderson4D.SmoothCutoff.r324RoutedEval_zeroShift_ledger (ρ : SmoothCutoff) {m : ℕ} (hm : 0 < m) (hm2 : m ≤ 2) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (lam : ℝ) {ε : ℝ}, 0 < ε → ε ≤ 1 → ∀ (α β : Z4), ∑' (pb : R324RefinedScheduleIndex m × ℕ), ρ.r324ZeroShiftGroupedWeight lam hm ε α β pb ≤ 16 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * (|lamEps lam ε| ^ (2 * m) * (K * ε⁻¹ ^ (4 * m)))

The grouped zero-shift mass ledger at m ≤ 2: the complete grouped L¹ ledger is priced by the raw covariance mass K·ε^{-4m}.

theorem Anderson4D.exists_r324RoutedZeroShiftWindowBound_one (ρ : SmoothCutoff) (lam : ℝ) : ∃ (C : ℝ), 0 < C ∧ R324RoutedZeroShiftWindowBound ρ lam 1 C

The zero-shift routed window ledger holds at order one.

theorem Anderson4D.exists_r324RoutedZeroShiftWindowBound_two (ρ : SmoothCutoff) (lam : ℝ) : ∃ (C : ℝ), 0 < C ∧ R324RoutedZeroShiftWindowBound ρ lam 2 C

The zero-shift routed window ledger holds at order two.

theorem Anderson4D.r324RoutedEval_tsum_finOne {H : Z4 → ℝ} (hH : Summable H) : (Summable fun (q : Fin 1 → Z4) => H (q 0)) ∧ ∑' (q : Fin 1 → Z4), H (q 0) = ∑' (k : Z4), H k

One-slot configuration sums collapse to plain lattice sums.

theorem Anderson4D.SmoothCutoff.r324RoutedEval_nonzeroMass_one (ρ : SmoothCutoff) (hm : 0 < 1) {ε CB : ℝ} (hε : 0 < ε) (hCB : ∀ (k : Z4), (1 + ‖z4EuclideanFrequency k‖ ^ 2) ^ 4 * ‖ρ.covarianceModeCoeff ε k‖ ≤ CB) (α β : Z4) (hexternal : α + β ≠ 0) (p : R324RefinedScheduleIndex 1) : ∑' (a : ρ.R324RefinedEndpointNonzeroRawConfiguration hm ε α β p), ρ.r324RefinedRawCovarianceRouteWeight hm ε p ↑a ≤ ↑(Nat.card (R324RefinedContractionIndex p)) * (2 * CB)

The endpoint-constrained order-one route mass. At m = 1 frequency conservation of endpoint-nonzero configurations pins the single increment key to α + β, hence the slot mode to ±(α + β); the surviving routed mass is the contraction-fibre cardinality times twice the marked slot value.

theorem Anderson4D.SmoothCutoff.r324RoutedEval_perSchedule_one (ρ : SmoothCutoff) (lam : ℝ) (hm : 0 < 1) {ε CB : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hCB : ∀ (k : Z4), (1 + ‖z4EuclideanFrequency k‖ ^ 2) ^ 4 * ‖ρ.covarianceModeCoeff ε k‖ ≤ CB) (α β : Z4) (hexternal : α + β ≠ 0) (hmtrunc : 1 ≤ truncOrder ε) (p : R324RefinedScheduleIndex 1) : ∑' (route : R324NonzeroRouteLabel 1), ρ.r324RefinedEndpointNonzeroRouteWeight lam hm ε α β hexternal hε hε1 hmtrunc p route ≤ 16 * paperFourthOrderModeDecay α * paperFourthOrderModeDecay β * (|lamEps lam ε| ^ (2 * 1) * (r324AllContractionInteriorSkeletonL1 1 * (↑(Nat.card (R324RefinedContractionIndex p)) * (2 * CB))))

Per-schedule routed weight ledger at m = 1: the corrected route weights of one refined schedule are worth the skeleton envelope times the endpoint-constrained mass.

theorem Anderson4D.exists_r324RoutedPerTermWindowBound_one (ρ : SmoothCutoff) (lam : ℝ) : ∃ (C : ℝ), 0 < C ∧ R324RoutedPerTermWindowBound ρ lam 1 C

The routed per-term window ledger holds at order one. The constant depends only on the cutoff.