jq
plain-language theorem explainer
The rational J-display sends a nonzero rational t to (t + t^{-1})/2 - 1. It is the native cost functional of Recognition Science evaluated on ℚ, matching the unique J forced by the Recognition Composition Law. Gauge-orbit classification and signed-power cost theorems cite it whenever a ratio-orbit cost is reduced to an explicit rational. The body is a one-line closed-form definition.
Claim. For $t \in \mathbb{Q}$ (with $t \neq 0$), the J-display is $J(t) := \dfrac{t + t^{-1}}{2} - 1 \in \mathbb{Q}$.
background
Recognition Science fixes a unique cost functional on positive scales by the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, together with normalization $J(1)=0$ and evenness under $t\mapsto t^{-1}$. The unique continuous solution is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$ (forcing step T5).
This module works in the Primitive Recognition Calculus (PRC) native-cost ledger over rational ratio orbits. Costs are compared by cross-display equality of rational values rather than by real-analytic identities. The present definition is simply that closed form, restricted to $\mathbb{Q}$, so that every later ledger identity can be checked by rational arithmetic.
Sibling facts in the same file record the elementary calculus of this display: value at $1$ and at $0$ (undefined or infinite), nonnegativity on positives, vanishing only at $\pm 1$, and the sign-flip identity $J(-t)=J(t)$ when defined.
proof idea
Pure definition: the body is the closed-form expression $(t + t^{-1})/2 - 1$ on $\mathbb{Q}$. No lemmas are applied.
why it matters
This is the concrete evaluation map that turns abstract native-cost objects into rationals. Downstream, cost_at_pos states that on a positive display the cost equals $J$ of the $k$-th power of the orbit representative; signedPowerNativeCost_toRat reduces every signed-power native cost to $J(\mathrm{signedPow}, m, q)$; and the exponent-two anchor identity charges $J(4)$ at the doubled-trace point. Those reductions feed the classification that the nondegenerate branch is a sign-extended power cost, and the separation of signed-power costs from pure sign-gauge costs.
In the forcing chain this is exactly the T5 J-cost, now available as a rational ledger primitive so that gauge-orbit theorems never leave $\mathbb{Q}$. It is also the cost that appears in the RCL identity and in the mass/yardstick ladder once the display is lifted back to positive reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.