traceRootDenominator_toRat
plain-language theorem explainer
The native ratio-orbit encoding of the trace-root denominator evaluates to the ordinary rational 3. Anyone deriving the linear root candidate χ(q)=(2T(2q)−T(q))/3 from the split-trace identity at axis 2 cites this display lemma. The proof is a short rewrite through orbit addition and the canonical displays of 2 and 1, finished by numeric normalization.
Claim. The ratio-orbit constant used as the denominator of the linear root candidate has rational display equal to $3$.
background
In the Primitive Recognition Calculus, rationals are carried as RatioOrbit values: a signed-orbit numerator over a nonzero distinction-nat denominator, with a verifier map toRat sending each orbit to an ordinary rational by integer division. Addition of orbits is compatible with that display: (a+b).toRat = a.toRat + b.toRat, and the unit orbit displays as 1; the orbit for 2 likewise displays as 2.
The surrounding module builds a native cost from a character via the doubled-trace functional $T(q)=\chi(q)+\chi(q)^{-1}$. At the distinguished axis where $\chi(2)=2$, solving the split-trace identity for the character produces the linear root candidate $\chi(q)=(2,T(2q)-T(q))/3$. The constant 3 in that formula is itself a ratio orbit (two plus one); this lemma records its rational display.
proof idea
Term-mode one-shot rewrite. Unfold the denominator orbit as the sum of the canonical orbits for 2 and 1; apply orbit-addition compatibility with toRat, then the simp facts that those two orbits display as 2 and 1; finish with norm_num to obtain $2+1=3$.
why it matters
Feeds the parent display theorem for the nonzero root candidate: once the denominator is known to be 3 in rationals, (traceRootCandidate T q).toRat expands exactly to $(2,(T(2q)).toRat-(T q).toRat)/3$. That identity is the bridge from the doubled-trace d'Alembert package to the claim that a native cost character is forced by its trace values, which is the local uniqueness engine of this module.
In the broader Recognition chain this sits under T5 J-uniqueness and the Recognition Composition Law: the same algebraic skeleton that forces $J(x)=(x+x^{-1})/2-1$ reappears here as a character-plus-inverse trace, and the factor 3 is the concrete coefficient after fixing $\chi(2)=2$. Without the denominator display, the candidate formula cannot be transported to verifier rationals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.