canonicalSelectedNativeCost_jq
plain-language theorem explainer
On every rational orbit, the verifier display of the canonical selected native cost equals the classical J-cost of that orbit's rational value. Structural-axiom proofs (positivity, monotonicity, sign-reversal) for the selected cost cite this bridge. One-line wrapper of the selection display theorem under the named J display.
Claim. For every rational orbit $q$, if $F$ is the canonical selected native cost, then the verifier rational of $F(q)$ equals $J\bigl(\mathrm{toRat}(q)\bigr)$, where $J(t)=\frac{t+t^{-1}}{2}-1$ is the J-display on rationals.
background
A RatioOrbit is an integer-numerator / nonzero-denominator display of a rational (K4.7). Its verifier map toRat sends the orbit to $\mathbb{Q}$ by ordinary division; the internal equality test is cross-multiplication.
The J-display on a rational is $J(t)=(t+t^{-1})/2-1$, written here as jq. This is the same closed form forced uniquely by the Recognition Composition Law in the T5 step of the forcing chain.
The canonical selected native cost is the native J-cost on ratio orbits with the unit orbit sent to the literal zero representative. Upstream, canonicalSelectedNativeCost_toRat already states that its verifier display equals $(t+t^{-1})/2-1$ on every orbit (both sides zero on the unit branch). This module's Part 3 records that the selected cost satisfies the structural ledger axioms; the present lemma is the display bridge those proofs use.
proof idea
One-line wrapper: apply canonicalSelectedNativeCost_toRat at $q$. That theorem already expands the selected cost by cases on whether $q$ displays as $1$, and reduces both branches to $(t+t^{-1})/2-1$. Unfolding the local definition jq t := (t+t^{-1})/2-1 makes the two right-hand sides identical, so no further algebra is needed.
why it matters
This is the rewrite hinge for the three structural certificates on the selected cost in the same ledger: sign-reversal, monotonicity, and positivity each open by rewriting both sides through this equality, then invoke the corresponding property of jq (jq_nonneg, jq_mono, and the sign-flip identity).
In the Recognition framework it pins the selected native cost to the T5 J-form $J(x)=\cosh(\log x)-1$ at the rational-display layer, so later uniqueness and minimality arguments can work entirely with the classical J calculus rather than the orbit-level selection definition. It does not itself prove uniqueness of $J$; it only identifies the already-chosen witness with that formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.