Unconditional bracket-harvest kit for the final hdet assembly

Pointwise central-frequency infrastructure for the R-324 routed branch:

• r324HdetAssembly_prod_eighthDecay_le — the product bracket: the product of per-key ⟨·⟩⁻⁸ factors is bounded by n⁴ times the bracket at the summed frequency (Weierstrass + Cauchy--Schwarz);
• r324HdetAssembly_exists_halfSymbol_sq_bracket — the half-symbol split: the squared cutoff symbol carries one full per-key ⟨·⟩⁻⁸;
• r324HdetAssembly_endpointLoss_mul_epsScale_le_paper — the natural ⟨ε‖·‖⟩⁻⁸ scale of the pointwise harvest dominates the paper's frozen ⟨ε²‖·‖⟩⁻⁸ bracket;
• lam-uniform replays of the proved order-one routed window ledgers, so the unconditional m = 1 countable routed output is available with a constant depending on the cutoff only (the proved statements quantify lam before the constant, which the hdet interface cannot absorb).

The product bracket

theorem Anderson4D.r324HdetAssembly_one_add_sum_le_prod {ι : Type u_1} (s : Finset ι) (x : ι → ℝ) (hx : ∀ i ∈ s, 0 ≤ x i) : 1 + ∑ i ∈ s, x i ≤ ∏ i ∈ s, (1 + x i)

Weierstrass product inequality: 1 + Σxᵢ ≤ Π(1 + xᵢ) for nonnegative xᵢ.

theorem Anderson4D.r324HdetAssembly_sq_sum_le_card_mul_sum_sq {n : ℕ} (a : Fin n → ℝ) : (∑ i : Fin n, a i) ^ 2 ≤ ↑n * ∑ i : Fin n, a i ^ 2

Cauchy--Schwarz on Fin n: (Σaᵢ)² ≤ n · Σaᵢ².

theorem Anderson4D.r324HdetAssembly_prod_eighthDecay_le {n : ℕ} (hn : 1 ≤ n) (a : Fin n → ℝ) : ∏ i : Fin n, eighthOrderFrequencyDecay (a i) ≤ ↑n ^ 4 * eighthOrderFrequencyDecay (∑ i : Fin n, a i)

The pointwise product bracket. For n ≥ 1 nonnegative key sizes, the product of the per-key ⟨·⟩⁻⁸ factors is bounded by n⁴ times the eighth-order bracket at the summed size: Π ⟨aⱼ⟩⁻⁸ ≤ n⁴ · ⟨Σ aⱼ⟩⁻⁸. Combined with momentum conservation (Σ ±(ε·keys) = ε·freq(α+β)) this harvests the central frequency bracket pointwise, with no zone split.

The half-symbol split

theorem Anderson4D.r324HdetAssembly_exists_halfSymbol_sq_bracket (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : R4), ‖fourierR4 ρ.toFun ξ‖ ^ 2 ≤ C * eighthOrderFrequencyDecay ‖SmoothCutoff.euclideanFrequency ξ‖

Half-symbol bracket. The squared cutoff symbol carries one complete per-key eighth-order bracket: ‖ρ̂(ξ)‖² ≤ C·⟨‖ξ‖⟩⁻⁸. One half of each squared symbol feeds the product bracket over the keys, the other half remains for the ‖ρ̂‖-weighted windows.

Coupling-uniform order-one routed window ledgers

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

Coupling-uniform replay of the proved exists_r324RoutedPerTermWindowBound_one: the constant is fixed before the coupling, as required by the hdet interface. The proof body is the proved one; only the quantifier order changes.

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

Coupling-uniform replay of the proved exists_r324RoutedZeroShiftWindowBound_one.

theorem Anderson4D.r324HdetAssembly_exists_countableRoutedOutput_one (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ (lam : ℝ) {ε : ℝ}, 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → 1 ≤ truncOrder ε → ∀ (α β : Z4), CountableCentralRoutedMomentReductionOutput ρ lam ε 1 α β (lamEps lam ε ^ 2 * (16 * C ^ 1 * lam ^ (2 * 1 - 2)) * r324EndpointLoss ε α β)

The coupling-uniform unconditional order-one routed output. One cutoff-only constant funds the countable central routed moment reduction output at m = 1 for every coupling, at the windowed amplitude of the proved interface.

Scale comparison: ⟨ε‖·‖⟩⁻⁸ dominates the paper bracket

theorem Anderson4D.r324HdetAssembly_endpointLoss_mul_epsScale_le_paper {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (α β : Z4) : r324EndpointLoss ε α β * eighthOrderFrequencyDecay (ε * ‖z4EuclideanFrequency (α + β)‖) ≤ paperDeterministicMomentDecay ε α β

The natural ε-scale bracket of the pointwise harvest, priced with the endpoint loss, is at least as strong as the frozen paper decay, whose bracket sits at scale ε².