primeEulerEvent_mem_finiteEulerLedger
plain-language theorem explainer
The theorem asserts that for positive real σ and finite prime list support, membership of p in support implies the Euler event of ratio p^{-σ} belongs to the events of the recursively built ledger. Number theorists constructing arithmetic-to-ledger bridges cite it to verify prime factors populate the finite ledger. The proof is by structural induction on the support list, splitting the membership hypothesis via List.mem_cons and unfolding the add_event recursion.
Claim. Let σ > 0. For any finite list of primes support and prime p, if p belongs to support then the recognition event with ratio p^{-σ} is among the events of the ledger obtained by successively adding, for each prime in support, the event of ratio p^{-σ} together with its reciprocal.
background
The module builds concrete finite ledgers from Euler prime factors. primeEulerEvent σ hσ p yields a RecognitionEvent whose source is 0, target is p, and ratio is (p : ℝ)^{-σ} (positive by the eigenvalue_pos lemma). finiteEulerLedger σ hσ support is defined recursively: the empty list yields the empty ledger, while a cons list applies add_event to the tail ledger and the head prime event. add_event appends both the supplied event and its reciprocal (source/target swapped, ratio inverted) while preserving double-entry balance.
proof idea
The term proof performs structural induction on the support list. The empty-list case dispatches the impossible membership hypothesis by cases. For a cons list q :: qs the membership hypothesis is split by List.mem_cons into head or tail. The head case substitutes p and simplifies using the definitions of finiteEulerLedger and add_event. The tail case applies the inductive hypothesis directly to the shorter list.
why it matters
This membership result is invoked by the downstream theorem primeEulerEvent_mem_sensorEulerLedger to populate the sensor-indexed ledger. It supplies the first concrete arithmetic ledger in the module, whose events are precisely the prime Euler terms p^{-σ} together with their reciprocals, guaranteeing balance by construction and zero net flow via the generic ledger conservation theorem. In the Recognition Science setting it furnishes the arithmetic bridge object whose recognition costs are given by J(p^{-σ}), feeding later ledger-balance and cost-positivity statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.