Fourier Symbol Lower Bounds

Establishes lower bounds on the Fourier symbol:

• w(t) ≥ 1/(2t) on (0,1] via hyperbolic inequalities (Lemma 10)
• ψ_λ(ξ) ≥ c₁ log|ξ| - c₂ for large |ξ| (Lemma 11, axiomatized)
• log(2+|ξ|) ≤ a + b · ψ_λ(ξ) frequency moment control (Corollary 12, axiomatized)
• ψ_λ(ξ) → ∞ as ξ → +∞

Reference: lamportform.tex, Section 7.2, lines 940–1057.

Auxiliary lemmas for the weight lower bound

theorem ConnesLean.sinh_le_mul_cosh {t : ℝ} (ht : 0 ≤ t) : Real.sinh t ≤ t * Real.cosh t

sinh t ≤ t · cosh t for t ≥ 0.

Proof: The function g(t) = t · cosh t - sinh t satisfies g(0) = 0 and g'(t) = t · sinh t ≥ 0 for t ≥ 0, so g is monotone on [0, ∞).

This is the key step in showing sinh t ≤ t · exp (t/2) and hence w(t) = exp(t/2)/(2 sinh t) ≥ 1/(2t).

theorem ConnesLean.exp_half_lt {t : ℝ} (ht1 : t ≤ 1) : Real.exp (t / 2) < 5 / 3

For t ≤ 1, exp(t/2) < 5/3.

From exp(1) < 2.72 < 25/9 = (5/3)², so exp(1/2)² = exp(1) < 25/9, hence exp(1/2) < 5/3 (both positive). For t ≤ 1, monotonicity gives exp(t/2) ≤ exp(1/2) < 5/3.

theorem ConnesLean.cosh_le_exp_half {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1) : Real.cosh t ≤ Real.exp (t / 2)

cosh t ≤ exp(t/2) for t ∈ [0, 1].

Key algebraic idea: set v = exp(t/2), then the inequality (v² + v⁻²)/2 ≤ v is equivalent to v⁴ + 1 ≤ 2v³, which factors as -(v-1)(v³ - v² - v - 1) ≥ 0. For v ∈ [1, 5/3), v²(v-1) < 50/27 < 2 ≤ v+1 ensures the second factor is nonpositive.

Weight lower bound (Lemma 10)

theorem ConnesLean.archWeight_ge_inv_two_t {t : ℝ} (ht : 0 < t) (ht1 : t ≤ 1) : 1 / (2 * t) ≤ archWeight t

The archimedean weight satisfies w(t) ≥ 1/(2t) for t ∈ (0, 1].

Proof chain:

1. sinh t ≤ t · cosh t (from sinh_le_mul_cosh)
2. cosh t ≤ exp(t/2) for t ∈ [0,1] (from cosh_le_exp_half)
3. Hence sinh t ≤ t · exp(t/2), so exp(t/2) / (2 sinh t) ≥ 1/(2t).

Reference: lamportform.tex, Lemma 10 (line 940).

Logarithmic growth (Lemma 11, axiomatized)

axiom ConnesLean.fourierSymbol_ge_log (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) : ∃ (c₁ : ℝ) (c₂ : ℝ), 0 < c₁ ∧ ∃ (ξ₀ : ℝ), 2 ≤ ξ₀ ∧ ∀ (ξ : ℝ), ξ₀ ≤ |ξ| → c₁ * Real.log |ξ| - c₂ ≤ fourierSymbol cutoffLambda ξ

Logarithmic growth of the Fourier symbol: for λ > 1, there exist constants c₁ > 0, c₂, and ξ₀ ≥ 2 such that ψ_λ(ξ) ≥ c₁ log|ξ| - c₂ for all |ξ| ≥ ξ₀.

Proof sketch (lamportform.tex, Lemma 11, lines 964–1021):

1. Drop the nonneg prime sum; restrict arch integral to (0, min(1,2L)).
2. Apply archWeight_ge_inv_two_t: ψ_λ(ξ) ≥ 4c₀ ∫₀^{t₀} (1/t) sin²(ξt/2) dt.
3. Substitute u = ξt/2, partition [0, R] into π-intervals where sin² ≥ 1/2.
4. Sum ≥ H_N/2 ≥ log(N)/2 where N ~ |ξ| (harmonic series lower bound).

Why axiom: All building blocks exist in Mathlib (integral_sin_sq, log_le_harmonic_floor, substitution lemmas) but assembly requires 150+ lines of integral manipulation.

Soundness: Sole precondition is 1 < cutoffLambda, matching Lemma 11. The existential conclusion (∃ c₁ c₂ ξ₀) cannot be vacuously satisfied. No structure parameters.

Frequency moment control (Corollary 12, axiomatized)

axiom ConnesLean.frequency_moment_control (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) : ∃ (a : ℝ) (b : ℝ), 0 < a ∧ 0 < b ∧ ∀ (ξ : ℝ), Real.log (2 + |ξ|) ≤ a + b * fourierSymbol cutoffLambda ξ

Energy controls a logarithmic frequency moment: there exist a, b > 0 such that log(2 + |ξ|) ≤ a + b · ψ_λ(ξ) for all ξ.

Proof sketch (lamportform.tex, Corollary 12, lines 1023–1057):

• For |ξ| ≥ ξ₀: log(2+|ξ|) ≤ log(3|ξ|) ≤ (ψ_λ(ξ) + c₂)/c₁ + log 3 (from fourierSymbol_ge_log).
• For |ξ| < ξ₀: log(2+|ξ|) ≤ log(2+ξ₀), a finite constant.
• Set b = 1/c₁, a = c₂/c₁ + log 3 + log(2+ξ₀).

The integral version (multiplying by |φ̂(ξ)|² and integrating) is deferred to the Fourier representation PR.

Soundness: Sole precondition is 1 < cutoffLambda, matching Corollary 12. The existential conclusion (∃ a b with positivity) cannot be vacuously satisfied. No structure parameters.

Derived: Fourier symbol tends to infinity

theorem ConnesLean.fourierSymbol_tendsto_atTop (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) : Filter.Tendsto (fun (ξ : ℝ) => fourierSymbol cutoffLambda ξ) Filter.atTop Filter.atTop

The Fourier symbol tends to +∞ as ξ → +∞.

Derived from fourierSymbol_ge_log: for any bound B, choose ξ₁ = max(ξ₀, exp((B + c₂)/c₁)), then for ξ ≥ ξ₁, ψ_λ(ξ) ≥ c₁ log ξ - c₂ ≥ B.

Combined with fourierSymbol_even, this gives ψ_λ(ξ) → ∞ as |ξ| → ∞.