canonicalSelectedNativeCost
plain-language theorem explainer
The canonical selected native cost sends each rational orbit to the PRC J-cost object, except the unit orbit (rational display 1), which is mapped to the literal zero representative. It is the non-vacuity witness for the full zero-calibrated prime-signed strengthened native-cost hypothesis class. Uniqueness and minimality arguments for the native cost cite it as the concrete inhabitant. The body is a one-line case split on the rational display.
Claim. For a ratio orbit $q$, define the selected native cost by $J(q)=\frac{q+q^{-1}}{2}-1$ whenever the rational display of $q$ is not $1$, and by the zero orbit whenever that display equals $1$.
background
A ratio orbit is an integer numerator over a nonzero distinction-orbit denominator; its verifier display toRat recovers the ordinary rational value by integer division. The PRC rational J-cost on such orbits is the orbit-level object $J(q)=((q+q^{-1})/2)-1$, built from native add, reciprocal, multiply-by-half, and subtract-one. That object is not yet the real-analytic uniqueness theorem; it is the discrete carrier used inside the primitive recognition calculus.
The module selects a native cost functional among candidates that satisfy zero-calibration, prime-signed, and strengthened structural hypotheses. The unit orbit (display value 1) is the fixed point of reciprocity, where the algebraic J formula evaluates to zero; the selection forces that case onto the literal zero representative so the witness is strictly zero-calibrated rather than merely J-zero up to display.
proof idea
Pure definition by case split: if the rational display of the input equals 1, return the zero ratio orbit; otherwise apply the PRC J-cost constructor on ratio orbits. No lemmas are invoked in the body. Downstream theorems then verify that this witness inhabits the various slim and sans-* hypothesis packages by reducing through the full-hypothesis certificate and the slim-iff-full equivalence.
why it matters
This is the concrete non-vacuity witness that makes the native cost selection package inhabited rather than empty. Downstream, the slim-hypothesis theorem and the slim package theorem both package it with the cross-equality-to-J fact to discharge non-vacuity. The minimality-certificate module further projects it into the sans-pair, sans-RCL, sans-sign, sans-two, and sans-zero classes, each proving the corresponding weakened hypothesis bundle is still non-empty.
In the Recognition forcing chain this sits under T5 (J-uniqueness): the selected object is the discrete J-cost $J(x)=(x+x^{-1})/2-1$, which is also $\cosh(\log x)-1$, forced as the unique cost compatible with the Recognition Composition Law once zero-calibration and sign structure are imposed. Without an explicit inhabitant, uniqueness targets would be vacuously true; this definition closes that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.