primeEulerEvent_cost_eq_J
plain-language theorem explainer
The theorem equates the recognition cost of a prime Euler event, built from a positive exponent σ and prime p, to the J-function applied directly to the ratio p^{-σ}. Researchers constructing explicit arithmetic ledgers from Euler factors would cite it when summing costs over finite prime supports. The proof is a one-line reflexivity after the event definition and cost function are unfolded.
Claim. For positive real σ and prime p, the cost of the recognition event whose ratio is p^{-σ} equals J(p^{-σ}), where J is the recognition cost function.
background
In the concrete Euler ledger module, a recognition event is constructed for each prime p with ratio p^{-σ} (positive σ) and source-target pair (0, p). The cost of any recognition event is defined as the J-function applied to its ratio. This supplies the first fully concrete bridge object: a finite, balanced arithmetic ledger indexed by the sensor strip coordinate, with double-entry balance by construction and zero net flow from the generic conservation theorem. Upstream results include the event_cost definition stating that cost equals J of the ratio, and the primeEulerEvent definition that builds the event with the specified positive ratio.
proof idea
The proof is a one-line wrapper that applies reflexivity after the definitions of primeEulerEvent and event_cost are expanded.
why it matters
This supplies the explicit per-event cost used by the downstream finiteEulerLedger_cost_formula_J to obtain the total ledger cost as twice the sum of J(p^{-σ}) over the support. It completes the arithmetic-to-ledger identification step in the module, furnishing positive nontrivial recognition costs and an explicit total-cost formula in J terms. The result instantiates the J-cost on Euler factors within the Recognition Science framework, consistent with the J-uniqueness property and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.