reciprocal_primeEulerEvent_mem_finiteEulerLedger
plain-language theorem explainer
If a prime p belongs to the support list for positive real σ, then the reciprocal of its Euler recognition event at σ belongs to the events of the finite Euler ledger built from that list. Researchers constructing arithmetic-to-ledger bridges in Recognition Science cite this when verifying double-entry balance for prime-indexed events. The proof proceeds by structural recursion on the support list, with direct simplification on the head case via add_event and recursive application on the tail.
Claim. Let σ > 0 be real. For any finite list of primes support and any prime p in support, if e denotes the recognition event with ratio p^{-σ}, then the reciprocal event of e (with swapped source and target and inverse ratio) belongs to the events of the ledger finiteEulerLedger(σ, support).
background
The module builds concrete Ledger objects whose events are Euler terms p^{-σ} together with their reciprocals, for finite prime supports and positive real σ. A RecognitionEvent carries source, target, and positive ratio; LedgerForcing.reciprocal swaps source and target while inverting the ratio. The add_event operation appends both an event and its reciprocal, preserving the double-entry invariant by construction. finiteEulerLedger is defined by folding add_event over the support list, starting from the empty ledger.
proof idea
The term proof matches on the support list. The empty-list case is discharged by contradiction on the membership hypothesis. For a cons cell q :: qs, it splits the membership assumption: when p equals the head it substitutes and simplifies using the definitions of finiteEulerLedger and add_event; when p lies in the tail it applies the same statement recursively to qs.
why it matters
This membership result is invoked by the downstream theorem that lifts the same property to sensorEulerLedger for a DefectSensor. It supplies the first fully concrete, balanced arithmetic ledger in the module, with zero net flow guaranteed by the generic ledger conservation theorem and positive J-costs for each prime event. The construction forms the initial arithmetic-to-ledger identification step before any connection to the phi-ladder or spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.