primeEulerEvent
plain-language theorem explainer
primeEulerEvent assembles the atomic RecognitionEvent for a prime p under positive real exponent σ, with source fixed at zero, target at p, and ratio exactly p to the power -σ. Number theorists building explicit Euler-product models or ledger embeddings of arithmetic data would cite this when constructing balanced finite ledgers. The definition is a direct structure instantiation that obtains the required positivity witness from the eigenvalue_pos result.
Claim. For positive real σ and prime p, the recognition event has source 0, target p, ratio p^{-σ}, and ratio positivity given by the eigenvalue positivity theorem.
background
RecognitionEvent is the structure with fields source and target in ℕ, ratio in ℝ, and a proof that the ratio is positive. The Concrete Euler Ledger module uses this to realize the first arithmetic-to-ledger step: each prime contributes one event whose ratio is the Euler factor p^{-σ} together with its reciprocal, so that double-entry balance holds by construction. The module documentation states that the resulting ledger is finite, balanced, and carries an explicit total cost in terms of J(p^{-σ}). Upstream, eigenvalue_pos proves (p : ℝ)^{-σ} > 0 for σ > 0 by real-power positivity, while Primes simply collects the set of natural numbers that are prime.
proof idea
The definition is a direct structure instantiation. It supplies source := 0, target := p, ratio := (p : ℝ)^{-σ}, and ratio_pos := eigenvalue_pos hσ p. No further tactics are required beyond the field assignments and the call to the upstream positivity lemma.
why it matters
This definition supplies the primitive events from which finiteEulerLedger is built by iterated addition, and from which the cost formula, membership theorems, and sensor-indexed ledger are derived. It realizes the module's stated goal of providing the first fully concrete bridge object: a real arithmetic ledger whose events are Euler factors, with positive nontrivial recognition cost and zero net flow by the generic ledger conservation theorem. Downstream results such as finiteEulerLedger_cost_formula and primeEulerEvent_cost_eq_J depend on it to obtain explicit expressions in terms of J. It therefore occupies the arithmetic-to-ledger identification step in the Recognition Science chain before any claim to RSPhysicalThesis is attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.