The frequency-independent cosine loss in R-324 Step 4

Paper §4.2, Step 4 keeps the Green multiplier ⟨β⟩⁻² outside the terminal primitive block. At that point the character factor is estimated only by |cos - 1| ≤ 2. Consequently the ordinary Proposition 4.1 majorant is integrated without a squared-distance weight, and the resulting loss is the paper's ε⁻² |log ε|⁻¹ loss.

This file deliberately does not use the sharper local quadratic character estimate: doing so here would incorrectly claim an additional frequency decay after the Green multiplier has already been retained.

Generic frequency-independent integral domination

theorem Anderson4D.norm_integral_mul_r324CharacterCos_sub_one_le_two_mul_of_abs_le {J M : T4 → ℝ} (β : Z4) (hJ : ∀ (u : T4), |J u| ≤ M u) (hint : MeasureTheory.Integrable M paperMeasure) : ‖∫ (u : T4), ↑(J u * (r324CharacterCos β u - 1)) ∂paperMeasure‖ ≤ 2 * ∫ (u : T4), M u ∂paperMeasure

A signed real kernel dominated by an integrable majorant loses at most the exact factor 2 after multiplication by the terminal cosine defect. The conclusion is a complex Bochner-integral bound, matching the terminal Fourier identity.

Ordinary Proposition 4.1 majorant

theorem Anderson4D.norm_integral_primitiveKernelDiff_mul_r324CharacterCos_sub_one_le_two_mul (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (supportConstant primitiveConstant : ℝ) (hε : 0 < ε) (hbound : PrimitiveKernelBounds ρ lam ε n hn G supportConstant primitiveConstant) (β : Z4) : ‖∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε n hn G u * (r324CharacterCos β u - 1)) ∂paperMeasure‖ ≤ 2 * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant n u ∂paperMeasure

The ordinary half of PrimitiveKernelBounds supplies exactly the majorant used in Step 4. In particular, the right-hand side has no distance weight and no hidden sign assumption.

theorem Anderson4D.exists_norm_integral_primitiveKernelDiff_mul_r324CharacterCos_sub_one_le_raw : ∃ (Cball : ℝ) (Creg : ℝ), 0 < Cball ∧ 0 < Creg ∧ ∀ (ρ : SmoothCutoff) (primitiveConstant supportConstant lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ), 0 < ε → 0 < supportConstant → 1 ≤ |Real.log ε| → PrimitiveKernelBounds ρ lam ε n hn G supportConstant primitiveConstant → ∀ (β : Z4), ‖∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε n hn G u * (r324CharacterCos β u - 1)) ∂paperMeasure‖ ≤ 2 * ((primitiveConstant * lam) ^ (2 * n) * ((Cball * supportConstant ^ 2 + Creg) * ε⁻¹ ^ 2 / |Real.log ε|))

Quantifier-honest numerical form of the preceding estimate. The integration constants are chosen once, before the cutoff, coupling, scale, order, primitive input, and pointwise-bound constants.

Full-pairing terminal adapter

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.norm_integral_terminalPrimitiveKernelDiff_mul_r324CharacterCos_sub_one_le_two_mul {ρ : SmoothCutoff} {C lam ε K A : ℝ} {q : ℕ} {κ : PartialPairing (Fin (2 * q))} {budget : R324FullPairingBudgetStopTrace κ} (data : R324FullPairingBudgetTerminalAdapter budget) (hε : 0 < ε) (supportConstant primitiveConstant : ℝ) (hbound : PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges supportConstant primitiveConstant) (β : Z4) : ‖∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges u * (r324CharacterCos β u - 1)) ∂paperMeasure‖ ≤ 2 * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant (residualBlockOrder data.geometry.terminalData.terminal.2) u ∂paperMeasure

The Step 4 loss specialized to the genuine terminal block of a full-pairing budget trace. The adapter fixes the retained block and its internal edges; PrimitiveKernelBounds supplies the ordinary J majorant.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.exists_norm_integral_terminalPrimitiveKernelDiff_mul_r324CharacterCos_sub_one_le_raw : ∃ (Cball : ℝ) (Creg : ℝ), 0 < Cball ∧ 0 < Creg ∧ ∀ (ρ : SmoothCutoff) (C lam ε K A : ℝ) (q : ℕ) (κ : PartialPairing (Fin (2 * q))) (budget : R324FullPairingBudgetStopTrace κ) (data : R324FullPairingBudgetTerminalAdapter budget) (supportConstant primitiveConstant : ℝ), 0 < ε → 0 < supportConstant → 1 ≤ |Real.log ε| → PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges supportConstant primitiveConstant → ∀ (β : Z4), ‖∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ (data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges u * (r324CharacterCos β u - 1)) ∂paperMeasure‖ ≤ 2 * ((primitiveConstant * lam) ^ (2 * residualBlockOrder data.geometry.terminalData.terminal.2) * ((Cball * supportConstant ^ 2 + Creg) * ε⁻¹ ^ 2 / |Real.log ε|))

Numerical Step 4 loss for every genuine full-pairing terminal adapter. The constants Cball and Creg precede every geometric and analytic parameter, so in particular they cannot depend on the trace, the cutoff, the coupling, or the terminal order.