primeEulerEvent_ratio
plain-language theorem explainer
The declaration shows that the ratio field of the prime Euler recognition event equals p to the power of negative sigma. Workers constructing the concrete arithmetic ledger in Recognition Science cite it to confirm that each prime factor contributes exactly the required Euler term. The proof reduces immediately to reflexivity by matching the field to the expression in the event constructor.
Claim. For positive real exponent $0 < σ ∈ ℝ$ and prime $p$, the ratio of the recognition event generated by the prime Euler factor equals $p^{-σ}$.
background
The Concrete Euler Ledger module formalizes the first arithmetic-to-ledger identification step. For any positive real exponent σ and finite prime support it builds an explicit LedgerForcing.Ledger whose recognition-event ratios are the Euler terms p^{-σ} together with their reciprocals. A DefectSensor with σ equal to its realPart then yields a finite balanced arithmetic ledger indexed by the same strip coordinate.
proof idea
The proof is a one-line reflexivity step that matches the ratio field directly to the expression used in the primeEulerEvent constructor.
why it matters
This declaration supplies the explicit bridge object described in the module documentation: a real arithmetic ledger built from prime Euler data with double-entry balance by construction. It ensures the recognition ratios align with the required Euler factors before the generic ledger conservation theorem is applied to obtain zero net flow. The step remains short of RSPhysicalThesis and does not yet invoke the Recognition Composition Law or the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.