onRatioOrbit_toRat
plain-language theorem explainer
The canonical primitive-recognition cost on a ratio orbit evaluates, under the rational display, to the classical J-formula $(q+q^{-1})/2-1$. Anyone proving reciprocal symmetry, the rational RCL surface, or continuum forcing of J cites this identity. The proof unfolds the orbit-cost constructor, rewrites through the rational transport lemmas for arithmetic and half, and closes by ring.
Claim. For every ratio orbit $q$, the rational display of the canonical PRC cost of $q$ equals $(r + r^{-1})/2 - 1$, where $r$ is the rational display of $q$.
background
In the primitive recognition calculus, positive ratios live as RatioOrbit objects: quotient-native multiplicative data with a rational display map toRat. The canonical cost constructor builds a new orbit from $q$ by the algebraic template of J, namely half of $q$ plus its reciprocal, minus one, all in orbit arithmetic.
The classical recognition cost is $J(x)=(x+x^{-1})/2-1$ (also written $\cosh(\log x)-1$). It is the unique continuous solution forced later by the Recognition Composition Law plus normalization; here one works only with the rational surface, before any real completion.
Sibling transport lemmas (add_toRat, mul_toRat, recip_toRat, half_toRat, one_toRat, sub_toRat) say that orbit arithmetic commutes with the rational display. This theorem is the cost-level instance of that commutation.
proof idea
Term-style tactic proof. Unfold the definition of the canonical orbit cost. Rewrite the resulting expression with the rational-transport lemmas for subtraction, multiplication, addition, reciprocal, the constant half, and the unit orbit. The goal collapses to a pure rational identity, discharged by ring.
why it matters
This is the quotient-native form of T5 J-uniqueness on ratio orbits: the PRC cost is literally the J-formula before any passage through classical Real. Downstream, canonical_cost_is_J_formula is a one-line rename of this identity; onRatioOrbit_crossEq uses it to show the cost respects cross-equivalence; normalized_invariant and canonical_rcl_surface rewrite through it to get GCD-invariance and the algebraic RCL surface $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ on nonzero orbits.
The continuum capstone forced_J_on_completion leans on the same identity: once a calibrated character produces a cost cross-equivalent to the canonical orbit cost, the display forces $J$. The still-open target is global identity from one-point calibration at two across independent prime directions; this lemma supplies the per-orbit J-formula that rigidity then propagates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.