reciprocal_primeEulerEvent_ratio
plain-language theorem explainer
The theorem shows that the ratio of the reciprocal of a prime Euler recognition event equals the prime raised to the positive real exponent sigma. Modelers constructing finite arithmetic ledgers from Euler products in Recognition Science cite this to confirm the inverse half of each event pair. The proof reduces at once by unfolding the reciprocal constructor and the prime event definition, then invoking real power negation and inversion cancellation.
Claim. Let $σ > 0$ be real and let $p$ be prime. If $e$ is the prime Euler recognition event carrying ratio $p^{-σ}$, then the ratio of the reciprocal event of $e$ equals $p^σ$.
background
The Concrete Euler Ledger module supplies the first explicit arithmetic-to-ledger bridge. For any positive real exponent σ and any finite set of primes it assembles a LedgerForcing.Ledger whose recognition events carry ratios exactly the Euler terms p^{-σ}, together with their reciprocal events. The module records that this object is balanced by construction and carries zero net flow by the generic ledger conservation theorem, while each prime event receives a positive J-cost.
proof idea
One-line wrapper that applies simp to the definitions of LedgerForcing.reciprocal and primeEulerEvent, together with the lemmas Real.rpow_neg and inv_inv.
why it matters
The result completes the ratio identity for the reciprocal half of every Euler pair inside the concrete ledger. It thereby supports the module's double-entry balance claim and supplies the explicit inverse ratios needed before any appeal to RSPhysicalThesis. The construction remains at the arithmetic identification step of the forcing chain and does not yet reach the phi-ladder or spatial dimension results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.