reciprocal_primeEulerEvent_mem_sensorEulerLedger
plain-language theorem explainer
The theorem asserts that reciprocals of prime Euler events for every supported prime belong to the event set of the sensor-indexed Euler ledger. Researchers establishing arithmetic-to-ledger bridges in Recognition Science would cite it when verifying reciprocity closure for concrete Euler systems. The proof is a one-line wrapper that unfolds the sensor ledger definition and invokes the finite-support membership result after list conversion.
Claim. Let $S$ be a defect sensor, let $F$ be a finite set of primes, and let $p$ be a prime in $F$. The reciprocal of the Euler recognition event for $p$ at the real part of $S$ lies in the event set of the Euler ledger constructed from $S$ and $F$.
background
The Concrete Euler Ledger module builds explicit LedgerForcing.Ledger objects whose recognition-event ratios are the Euler terms $p^{-σ}$ together with their reciprocals, for $σ$ equal to the real part of a DefectSensor and any finite prime support. The sensorEulerLedger function assembles these into a finite balanced ledger with zero net flow by the generic conservation theorem. Upstream, LedgerForcing.reciprocal defines the reciprocal event by swapping source and target while inverting the ratio, while primeEulerEvent produces the forward event with positive ratio $p^{-σ}$.
proof idea
The proof is a one-line wrapper. It unfolds the definition of sensorEulerLedger and applies exact reciprocal_primeEulerEvent_mem_finiteEulerLedger after mapping the Finset support to a list and using simpa to discharge the membership hypothesis.
why it matters
This membership result feeds directly into sensorEulerLedger_identification, the first concrete arithmetic identification theorem that establishes balance, zero net flow, and explicit prime-event membership for the constructed ledger. It is also used to build concreteDirectedEulerLedgerSystem and to prove reciprocity closure under support enlargement. In the Recognition Science framework it supplies the reciprocity half of the arithmetic-to-ledger bridge that precedes RSPhysicalThesis, ensuring every supported prime contributes both a forward Euler event and its reciprocal with positive J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.