cost
plain-language theorem explainer
Total recognition cost of a multiset of canonical events under an arbitrary ratio weight. Cosmology and action-principle results cite it as the additive cell functional whose exact preservation under rung coarsening is T-1. The body is a one-line map-and-sum over event ratios.
Claim. Given a ratio weight $w_r:\mathbb{R}\to\mathbb{R}$ and a multiset $m$ of recognition events (each a directed posting with a positive ratio), the total cost is $\sum_{e\in m} w_r(e_{\mathrm{ratio}})$.
background
Module T-1 formalizes rung-coarsening for the scale-adaptive Cosmogenesis engine: a recognition cell is a multiset of canonical events, and a block map partitions them into internal (both endpoints in one coarse block) and cross (promoted to coarse events with the same ratio). Conserved functionals of the cell must be unchanged under coarsen/refine.
An Event is a directed posting source → target carrying a positive ratio; the double-entry reciprocal is implicit. The weight wr is the engine's ratio cost, typically the doubled J-cost $J(x)=(x+x^{-1})/2-1$ from the forcing chain (T5). Sibling foundation defs assign the same J-cost to recognition events and multiplicative recognizers.
This cost is the additive lift of that weight to a whole multiset: map each event to wr of its ratio, then sum. It is the instance used for total-cost preservation and exact cost partition in T-1.
proof idea
Pure definition: apply the weight to each event ratio via multiset map, then take the multiset sum. No lemmas, no tactics.
why it matters
T-1 needs an explicit additive cost so that round-trip identity implies cost preservation and so that internal-plus-cross costs reassemble exactly (cost_partition). Downstream, the same functional feeds Euler–Lagrange work on the cost-rate action $S[\gamma]=\int J(\gamma),dt$ (constant-1 geodesic, uniqueness of the cost-rate EL solution) and acoustics certificates that package non-negativity and reciprocity of speech/pitch J-cost. In the RS spine it is the cell-level total that must stay exact when the ledger is coarsened one phi-rung, tying Cosmogenesis T-1 to the J-uniqueness landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.