eigenvalue_lt_one
For any real σ > 0 and prime p the real number p raised to -σ is strictly less than 1. Researchers embedding the classical Euler product into the Recognition Science carrier framework cite this to guarantee that each local factor 1 - p^{-σ} remains nonzero. The short tactic proof first casts the prime property p > 1 into the reals then applies the standard real-power inequality for bases greater than one and negative exponents.
claimLet σ > 0 be real and let p be prime. Then p^{-σ} < 1.
background
The module EulerInstantiation embeds the classical Euler product for the Riemann zeta function into the abstract annular cost and carrier framework. Core objects include the prime sum P(σ) = ∑_p p^{-σ} and the Hilbert-Schmidt norm squared ∑_p p^{-2σ}. The theorem sits inside the layer that converts concrete prime factors into a holomorphic nonvanishing carrier C(s) = det₂²(I - A(s)) on Re(s) > 1/2. The local setting is the instantiation chain primes → A(s) Hilbert–Schmidt → det₂ convergent → C(s) holomorphic nonvanishing, which makes the cost-covering axiom applicable.
proof idea
The proof is a two-step tactic. It first obtains 1 < p as a real by exact_mod_cast on the prime property one_lt. It then applies Real.rpow_lt_one_of_one_lt_of_neg to the negative exponent -σ.
why it matters in Recognition Science
This supplies the strict inequality needed for the prime Euler event ratio to lie below one and for the logarithmic derivative bounds in det2_log_factor_bound. It appears in the chain that establishes the EulerCarrier interface and thereby makes the cost-covering axiom applicable, yielding the conditional Riemann hypothesis. The parent theorems are primeEulerEvent_ratio_lt_one and det2_log_factor_bound. It touches the nonvanishing step required for the T0-T8 forcing chain by ensuring no zero factors appear in the product.
scope and limits
- Does not establish summability of the prime sum for σ > 1/2.
- Does not extend to complex σ with nonzero imaginary part.
- Does not address convergence of the full Euler product.
- Does not prove the Riemann hypothesis itself.
Lean usage
theorem primeEulerEvent_ratio_lt_one {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) : (primeEulerEvent σ hσ p).ratio < 1 := by simpa [primeEulerEvent] using eigenvalue_lt_one hσ pformal statement (Lean)
78theorem eigenvalue_lt_one {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
79 (p : ℝ) ^ (-σ) < 1 := by
proof body
Tactic-mode proof.
80 have hp_one : (1 : ℝ) < p := by
81 exact_mod_cast p.prop.one_lt
82 exact Real.rpow_lt_one_of_one_lt_of_neg hp_one (by linarith)
83
84/-- Each eigenvalue p^{−s} is positive for σ > 0. -/