event_cost
plain-language theorem explainer
The definition assigns to each recognition event its cost by applying the J functional to the event ratio. Researchers deriving double-entry ledger structure from J-symmetry cite this when summing costs or proving reciprocity in Recognition Science. It is a direct one-line definition delegating entirely to the pre-established J cost functional.
Claim. For a recognition event $e$ with positive ratio $r_e$, the cost is $J(r_e)$ where $J(x) = (x + x^{-1})/2 - 1$.
background
The Ledger Forcing module shows that J-symmetry forces double-entry ledger structure. A RecognitionEvent is a structure with source and target agents plus a positive real ratio. The J functional is defined by $J(x) = (x + x^{-1})/2 - 1$ and satisfies $J(x) = J(1/x)$ for $x > 0$. Upstream results include the reciprocal event map (which inverts the ratio) and the J_symmetric property from CostAlgebra.
proof idea
One-line definition that applies the J cost functional directly to the ratio field of the RecognitionEvent structure.
why it matters
This supplies the per-event cost used by ledger_cost and the reciprocity theorem, which together establish the ledger_forcing_principle. That principle derives balanced ledgers with zero total cost from J-symmetry, linking to the Recognition Science chain where J-uniqueness forces the eight-tick octave and double-entry conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.