primeEulerEvent_cost_pos
plain-language theorem explainer
Prime Euler events built from positive real exponent σ and any prime p carry strictly positive cost under the ledger forcing map. Researchers constructing the arithmetic-to-physical ledger bridge cite this when confirming each prime term adds a nontrivial positive contribution to total ledger cost. The proof applies the general nontrivial recognition positivity lemma to the constructed event together with its ratio-not-one property, then simplifies the two cost definitions.
Claim. For any real number $σ > 0$ and any prime $p$, the ledger event cost of the prime Euler event satisfies $0 < J(p^{-σ})$, where $J$ denotes the recognition cost function on positive reals.
background
The module constructs concrete finite ledgers whose recognition events have ratios given by Euler factors $p^{-σ}$ together with their reciprocals. The event cost is defined as $J$ applied to the event ratio, where $J(x) = (x + x^{-1})/2 - 1$ is the standard Recognition Science cost function. The upstream lemma nontrivial_recognition_positive_cost states that any recognition event whose ratio differs from 1 has positive recognition cost. The module doc-comment notes that this supplies the first fully concrete bridge object: a real arithmetic ledger with double-entry balance and positive nontrivial recognition cost for each prime event.
proof idea
The tactic proof introduces an auxiliary fact that the recognition cost of the prime Euler event is positive by applying nontrivial_recognition_positive_cost to the event and the already-established ratio_ne_one property. A single simpa step then rewrites recognition_cost as event_cost using the two definitions and closes the goal.
why it matters
This result supplies the required positivity of each prime contribution inside the concrete Euler ledger, the first arithmetic-to-ledger identification step described in the module doc-comment. It directly supports the subsequent finiteEulerLedger constructions and the claim of zero net flow via generic ledger conservation. The positivity is a prerequisite for any later comparison with the Berry creation threshold or the phi-ladder mass formula, though the declaration itself stops short of proving the full RSPhysicalThesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.