traceRootCandidate_toRat_of_nonzero
plain-language theorem explainer
When a ratio orbit is nonzero under the rational display, the trace-root candidate of a map T at that orbit has rational value (2·T(2q) − T(q))/3. Downstream uniqueness lemmas cite this identity to check multiplicativity, normalization, the unit point, reciprocity, and the linear-root quadratic target. The proof is a short rewrite through the candidate definition and the RatioOrbit-to-ℚ transport lemmas, finished by ring.
Claim. Let $T$ be a map on ratio orbits and let $q$ be a ratio orbit whose rational display satisfies $q_{\mathbb{Q}} \neq 0$. Then the rational display of the trace-root candidate of $T$ at $q$ equals $\bigl(2\,T(2\cdot q)_{\mathbb{Q}} - T(q)_{\mathbb{Q}}\bigr)/3$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). The map toRat is a verifier display sending such an orbit to a rational by casting numerator and denominator; the internal equality notion remains cross-multiplication. Arithmetic on orbits (mul, sub, recip) transports exactly to the corresponding operations on rationals via the lemmas mul_toRat, sub_toRat, and recip_toRat.
This module builds native-cost uniqueness from a doubled-trace root problem. A candidate root is extracted from a map $T$ on ratio orbits by a linear combination that, on the rational display, should recover the unique solution of a repaired doubled-trace equation. The constant two is the orbit display of $2$, with two_toRat fixing its rational value.
The local setting is the PRC native-cost uniqueness development: one shows that any $T$ obeying doubled-trace hypotheses and cross-equation respect yields a candidate that matches the native $J$-cost character on ratio orbits.
proof idea
Term/tactic hybrid, essentially a definitional transport. First rewrite the candidate definition and take the nonzero branch via if_neg hq (the hypothesis $q_{\mathbb{Q}}\neq 0$). Then push toRat through the arithmetic skeleton: mul_toRat twice (for the $2\cdot q$ factor and the outer scaling), sub_toRat, two_toRat, recip_toRat, and the denominator lemma traceRootDenominator_toRat. Close with norm_num to clear the concrete integer coefficients and ring to identify the resulting rational expression with $(2,T(2q){\mathbb{Q}}-T(q){\mathbb{Q}})/3$.
why it matters
This identity is the rational-display engine for the repaired doubled-trace root. Five sibling theorems apply it under doubled-trace hypotheses and cross-equation respect: the candidate is multiplicative on products, invariant under distinction-nat normalization, fixes the unit orbit, satisfies the linear-root quadratic target, and behaves correctly under reciprocal (via the companion traceRootCandidate_recip_toRat_of_nonzero).
In the Recognition framework this sits inside native-cost uniqueness for the Primitive Recognition Calculus, the discrete precursor to T5 $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law). Establishing that the only map compatible with the doubled-trace root is the native cost character closes the algebraic side of forcing a unique cost before the continuum $J$-cost and the phi fixed point are recovered.
No scaffolding remains on this lemma itself; it is a proved transport step that the uniqueness chain repeatedly invokes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.