Quantitative character cosine estimate for R-324

This file supplies the deterministic Fourier estimate used at the terminal cosine step of paper §4.2. With the project's conventions

• T4 = Fin 4 → AddCircle (2π),
• charT4 β u = ∏ i, exp (I * βᵢ * uᵢ),
• paperModeNormSq β = ∑ i βᵢ², and
• torusDistSq u = ∑ i (torusLift u i)²,

the canonical representative gives the exact identity charT4 β u = exp (I * ∑ i βᵢ * torusLift u i). Cauchy--Schwarz and 1 - cos θ ≤ θ² / 2 then give

|r324CharacterCos β u - 1| ≤ (1 / 2) * paperModeNormSq β * torusDistSq u.

The absolute constant 1 / 2 is the sharp scalar cosine constant. No compatibility or non-wrapping hypothesis is needed: the only representative fact used below is the proved quotient identity AddCircle.coe_equivIco. The final lemmas package the pointwise estimate as a norm-of-integral bound for either half of PrimitiveKernelBounds.

Exact phase identity and scalar estimate

theorem Anderson4D.charT4_eq_exp_dot_torusLift (β : Z4) (u : T4) : charT4 β u = Complex.exp (Complex.I * ↑(∑ i : Fin dim, ↑(β i) * torusLift u i))

A product character is the exponential of the dot product with the canonical componentwise lift. This is an exact quotient identity, not a choice of a locally compatible lift.

theorem Anderson4D.norm_charT4_sub_one_le_abs_dot_torusLift (β : Z4) (u : T4) : ‖charT4 β u - 1‖ ≤ |∑ i : Fin dim, ↑(β i) * torusLift u i|

First-order character distance, expressed without choosing any noncanonical lift.

theorem Anderson4D.sq_abs_dot_torusLift_le (β : Z4) (u : T4) : |∑ i : Fin dim, ↑(β i) * torusLift u i| ^ 2 ≤ paperModeNormSq β * torusDistSq u

Cauchy--Schwarz in the exact frequency/distance normalizations used by the paper.

theorem Anderson4D.two_mul_abs_r324CharacterCos_sub_one_eq_norm_sq (β : Z4) (u : T4) : 2 * |r324CharacterCos β u - 1| = ‖charT4 β u - 1‖ ^ 2

For a unit-modulus character, twice the cosine defect is exactly the squared chordal distance to 1.

theorem Anderson4D.abs_r324CharacterCos_sub_one_le_half_mul (β : Z4) (u : T4) : |r324CharacterCos β u - 1| ≤ 1 / 2 * paperModeNormSq β * torusDistSq u

Terminal cosine estimate. The constant 1 / 2 is the sharp one-dimensional cosine constant; Cauchy--Schwarz introduces no further dimension-dependent loss.

theorem Anderson4D.abs_r324CharacterCos_sub_one_le_two (β : Z4) (u : T4) : |r324CharacterCos β u - 1| ≤ 2

The frequency-independent unit-circle bound.

theorem Anderson4D.abs_r324CharacterCos_sub_one_le_min (β : Z4) (u : T4) : |r324CharacterCos β u - 1| ≤ min 2 (1 / 2 * paperModeNormSq β * torusDistSq u)

The local quadratic estimate and the global unit-circle estimate in the usual single min envelope.

Majorant and integral interfaces

theorem Anderson4D.paperModeNormSq_nonneg (β : Z4) : 0 ≤ paperModeNormSq β

theorem Anderson4D.abs_mul_r324CharacterCos_sub_one_le_of_abs_le {J M : T4 → ℝ} (β : Z4) (u : T4) (hJ : |J u| ≤ M u) : |J u * (r324CharacterCos β u - 1)| ≤ 1 / 2 * paperModeNormSq β * (torusDistSq u * M u)

Pointwise cosine domination for any signed real kernel controlled by a nonnegative majorant. Nonnegativity of M u follows from the stated absolute-value bound.

theorem Anderson4D.integrable_torusDistSq_mul_of_integrable {M : T4 → ℝ} (hM : MeasureTheory.Integrable M paperMeasure) : MeasureTheory.Integrable (fun (u : T4) => torusDistSq u * M u) paperMeasure

Multiplication by the bounded torus distance preserves integrability. This is the small adapter needed for both explicit Proposition 4.1 majorants.

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

Direct Bochner-integral domination by a squared-distance-weighted majorant. The complex cast matches the terminal cosine identity.

theorem Anderson4D.norm_integral_primitiveKernelDiff_mul_r324CharacterCos_sub_one_le (ρ : 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‖ ≤ 1 / 2 * paperModeNormSq β * ∫ (u : T4), torusDistSq u * primitiveKernelMajorant primitiveConstant lam ε supportConstant n u ∂paperMeasure

The ordinary half of PrimitiveKernelBounds, fed directly into the terminal cosine integral estimate.

theorem Anderson4D.norm_integral_primitiveKernelInsertedDiff_mul_r324CharacterCos_sub_one_le (ρ : 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), ↑(primitiveKernelInsertedDiff ρ lam ε n hn G u * (r324CharacterCos β u - 1)) ∂paperMeasure‖ ≤ 1 / 2 * paperModeNormSq β * ∫ (u : T4), torusDistSq u * primitiveInsertedMajorant primitiveConstant lam ε supportConstant n u ∂paperMeasure

The inserted half of PrimitiveKernelBounds, fed directly into the same terminal cosine integral estimate.