eigenvalue_lt_one
plain-language theorem explainer
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.
Claim. Let σ > 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.