Jcost
plain-language theorem explainer
Local alias of the Recognition Science cost on a positive real ratio: J(x)=(x+x^{-1})/2-1. Cosmology and acoustics modules cite it as the ledger cost of a forced posting or measured-to-expected ratio. The body is a one-line arithmetic definition, matching the unique T5 cost functional.
Claim. Define the recognition cost of a real ratio $x$ by $J(x) = \frac{x + x^{-1}}{2} - 1$.
background
Module T-3 (RefineTrigger) removes the free tolerance from scale-adaptive cosmogenesis. Descent is forced exactly where a block carries an internal posting; the block's recognition demand is the J-cost of those postings, and the law-given rule is descend iff demand > 0. The threshold is structurally zero, read off the ledger.
The cost functional itself is the unique continuous solution of the Recognition Composition Law fixed at T5 of the forcing chain: $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Upstream, Cost.Jcost is the same formula; ObserverForcing and MultiplicativeRecognizerL4 take event or comparator cost to be this J. RungCoarsen sums a ratio weight (typically doubled J) over multiset events to get total cell cost.
In this file the def is restated so demand, losslessness, and the epsilon-unsafety lemmas can name J without importing the global Cost module at every use site.
proof idea
Definition, not a theorem. The body is the closed-form arithmetic expression $(x + x^{-1})/2 - 1$ on $\mathbb{R}$. No tactics, no lemmas. Sibling facts jcost_pos and jcost_arbitrarily_small_positive then prove positivity off the identity ratio and that positive values can be arbitrarily small.
why it matters
J is the scalar that turns a forced internal posting into a recognition demand. T-3's law-given trigger (descend iff demand > 0) and the uniqueness of the zero threshold (lossless_iff, lossless_law, descendLaw_necessary, epsilon_unsafe) all read off this cost. Without it there is no ledger quantity whose vanishing marks identity and whose positivity forces refinement.
Downstream it is the domain cost across acoustics: harmonic distortion, voice range, middle C, A4, consonance, pitch JND, and room impulse response all set domainCost or pitchCost to $J(\mathrm{measured}/\mathrm{expected})$. That reuse is intentional: the same T5 functional scores ratio mismatch in cosmology cells and in frequency ratios.
Framework landmark: T5 J-uniqueness and the RCL $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Local role is the demand kernel of T-3 in the Cosmogenesis north-star spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.