rationalTrace
plain-language theorem explainer
Defines the doubled trace of a ratio-orbit endomorphism as a real-valued function of ordinary rationals: embed the rational into a ratio orbit, then take the real display of the native doubled trace. Downstream gauge-orbit and character-classification theorems cite it whenever they need the cost character on Q rather than on abstract orbits. The body is a one-line composition of the two maps.
Claim. Given an endomorphism $F$ of ratio orbits and a rational $x\in\mathbb{Q}$, the rational doubled trace is the real number obtained by sending $x$ to its ratio-orbit section and then taking the real display of the carrier-valued doubled trace of $F$ at that orbit.
background
In the real-character factorization of the Recognition cost, ratio orbits are the native carrier for rational displays: each is an integer numerator over a nonzero distinction-nat denominator. The map from classical rationals into that carrier is a verifier-backed section (not a new primitive), used to test whether the character interface already admits classical rational countermodels.
The doubled trace of an endomorphism $F$ is first computed in the native carrier, then projected to a real via the real display of that carrier value. The present definition simply composes those two steps so that the doubled trace can be written as an ordinary function $\mathbb{Q}\to\mathbb{R}$.
Local setting is the Cost module on real character factorization: one studies which endomorphisms of ratio orbits can serve as Recognition cost characters, and when their traces force power-law behaviour on positive rationals.
proof idea
One-line definitional wrapper: apply the ratio-orbit section of the input rational, then apply the real display of the carrier-valued doubled trace. No lemmas or tactics beyond that composition.
why it matters
This is the bridge that lets gauge-orbit classification work with classical rationals. Parent results in GaugeOrbitClassification use it constantly: the cost display is the rational doubled trace halved and shifted; degeneracy of the anchor is the equality of the doubled trace at two with two; existence of a natural exponent and multiplicativity on positive rationals both take nondegeneracy as rationalTrace F 2 \neq 2; positivity of charge at orbit two is read off the same value. Without an honest $\mathbb{Q}\to\mathbb{R}$ doubled trace, the six-exponentials route from a real exponent to a natural power law on positive displays would have no classical interface. It sits in the cost/character layer that feeds the J-uniqueness and native-cost uniqueness story (T5 / RCL), not in the geometric forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.