canonical_cost_is_J_formula
plain-language theorem explainer
On any ratio orbit the canonical primitive-recognition cost, read in rational display, equals the classical J-formula (q + q^{-1})/2 - 1. Foundation authors cite this whenever they need the quotient-native T5 cost without leaving the rational/orbit layer or invoking Mathlib Real. The proof is a one-line term that applies the existing orbit-to-rational cost identity.
Claim. For every ratio orbit $q$, the canonical PRC cost on $q$, displayed as a rational, equals $\frac{q_{\mathbb{Q}} + q_{\mathbb{Q}}^{-1}}{2} - 1$, where $q_{\mathbb{Q}}$ is the rational representative of the orbit. The identity is native to the quotient and does not route through classical $\mathbb{R}$.
background
Primitive Recognition Calculus equips ratio orbits with a canonical cost functional. A ratio orbit is an equivalence class of positive rational ratios under the ledger identification; its rational display toRat picks a representative. The cost is evaluated on that orbit and then re-displayed as a rational, staying inside the quotient-native arithmetic rather than Mathlib's completed reals.
The target formula is the Recognition Science J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely at T5 of the unified forcing chain and obeying the Recognition Composition Law. Upstream, the identity and reciprocal automorphisms of the cost algebra both generate the same cost on orbits, which is why the formula is reciprocal-symmetric by construction.
This module sits in the continuum completion layer: it records that the discrete PRC cost already matches the classical J display before any real completion or character-rigidity argument is applied.
proof idea
Term-mode one-liner. The goal is definitionally the statement of the upstream lemma that converts the canonical cost on a ratio orbit into its rational display; the proof simply applies that lemma to the given orbit. No algebraic expansion, case split, or real-analysis step is required.
why it matters
Pins the rational display of the canonical PRC cost to the T5 J-formula inside the quotient, before continuum completion. Downstream siblings in the same module (forced J on the completion, calibrated character forces J, one-point calibration to a global identity) rely on having this native formula available so that character rigidity and completion arguments transport the same J rather than a different cost shape.
In the broader framework this is the discrete, Mathlib-Real-free witness that the recognition cost is already $J(x)=(x+x^{-1})/2-1$ on ratio orbits, matching the unique solution of the Recognition Composition Law. It therefore anchors the continuum forcing package to the same functional that later yields $\varphi$, the eight-tick octave, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.