primeEulerEvent_ratio_lt_one
plain-language theorem explainer
The theorem shows that for any positive real exponent σ and any prime p the ratio of the associated prime Euler recognition event is strictly less than 1. Researchers building concrete arithmetic ledgers in Recognition Science cite it to confirm each prime factor yields a nontrivial event. The proof is a one-line wrapper that unfolds the event definition and applies the eigenvalue inequality.
Claim. For every real number σ > 0 and every prime p, if E is the recognition event whose ratio equals p^{-σ}, then the ratio of E satisfies p^{-σ} < 1.
background
The module constructs the first concrete bridge from arithmetic data to a Recognition Science ledger. For positive real σ and any finite set of primes it assembles a LedgerForcing.Ledger whose recognition events carry ratios p^{-σ} together with their reciprocals; the resulting object is balanced by construction and has zero net flow. The definition primeEulerEvent packages each prime factor as a RecognitionEvent with source 0, target p, and ratio (p : ℝ)^(-σ). The upstream result eigenvalue_lt_one states that each such p^{-σ} is strictly less than 1 whenever σ > 0, which is the key inequality used here.
proof idea
The proof is a one-line wrapper. It unfolds the definition of primeEulerEvent via simpa and directly invokes the upstream theorem eigenvalue_lt_one on the same hypotheses σ > 0 and prime p.
why it matters
The result guarantees that every prime Euler event is nontrivial, which is required for the concrete Euler ledger to be a genuine recognition object. It is invoked by the sibling theorem primeEulerEvent_ratio_ne_one to obtain the strict inequality ratio ≠ 1. Within the Recognition Science framework the lemma supplies the first arithmetic-to-ledger identification step that precedes the full physical thesis; it relies on the eigenvalue bound that ensures each factor (1 - p^{-σ}) is nonzero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.