eigenvalue_pos
plain-language theorem explainer
For positive real σ and any prime p the quantity p^{-σ} is strictly positive. Workers building the Euler product instantiation of the Recognition Science carrier cite this to guarantee that each prime factor supplies a positive ratio in the recognition event. The proof is a one-line term application of real rpow positivity after casting the prime to a positive real.
Claim. For any real number $σ > 0$ and any prime number $p$, the real number $p^{-σ}$ is positive.
background
The EulerInstantiation module realizes the abstract RS carrier and cost structures by instantiating the Euler product for ζ(s) inside the AnnularCost and CostCoveringBridge framework. Primes serve as the basic carriers; each prime p contributes the factor p^{-σ} to the Hilbert-Schmidt operator A(s) whose regularized determinant yields the holomorphic non-vanishing function C(s) on Re(s) > 1/2. The module therefore converts the arithmetic data of primes into the EulerCarrier interface required for the cost-covering axiom and the conditional Riemann hypothesis.
proof idea
The proof is a term-mode one-liner: it invokes Real.rpow_pos_of_pos on the positive real base obtained by casting the Nat.Prime property and on the arbitrary real exponent -σ.
why it matters
The lemma supplies the positivity hypothesis used by primeEulerEvent to construct the basic recognition event whose ratio is exactly p^{-σ}. It is also called inside the proof of det2_log_factor_bound. In the Recognition Science setting it closes the arithmetic positivity step that precedes convergence of the Hilbert-Schmidt norm and the carrier log series for σ > 1/2, thereby advancing the instantiation chain from primes to the conditional RH.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.