primeEulerEvent_ratio_ne_one
plain-language theorem explainer
primeEulerEvent_ratio_ne_one establishes that the ratio of any prime Euler event is never 1 for positive real exponent σ. Ledger constructors building concrete Euler data in Recognition Science cite it to guarantee that each event is nontrivial. The proof is a one-line wrapper that invokes the companion strict inequality theorem and applies the ne tactic.
Claim. For real number $σ > 0$ and prime $p$, let $r$ be the ratio of the recognition event with source 0, target $p$, and $r = p^{-σ}$. Then $r ≠ 1$.
background
The Concrete Euler Ledger module constructs an explicit LedgerForcing.Ledger from prime Euler factors for any positive real exponent σ. For each prime p the primeEulerEvent supplies a RecognitionEvent whose ratio equals p^{-σ} (positive by eigenvalue_pos) together with its reciprocal. The module supplies the first concrete arithmetic-to-ledger bridge object that is balanced by construction and has zero net flow by the generic conservation theorem.
proof idea
The proof is a one-line wrapper that applies primeEulerEvent_ratio_lt_one (which shows the ratio is strictly less than 1) and then uses the ne tactic to obtain inequality to 1.
why it matters
It is invoked by primeEulerEvent_cost_pos to feed nontrivial_recognition_positive_cost and conclude that each prime Euler event carries positive recognition cost. The module documentation positions the result inside the concrete bridge that supplies positive nontrivial recognition cost for every prime event before the full RSPhysicalThesis is addressed. In the Recognition Science framework it ensures the ledger events satisfy the nontriviality condition required by the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.