rationalTrace_eq_traceDisplay
plain-language theorem explainer
Under anchor-free native-cost hypotheses, the doubled cost trace on a ratio orbit equals the same trace evaluated at that orbit's rational display. Cost and real-character factorization proofs cite it to move freely between orbit and rational presentations. The argument is a short cross-equality reduction: the two inputs share a rational, so the display is invariant.
Claim. Let $F$ map ratio orbits to ratio orbits and satisfy the anchor-free native-cost pack (base without two, sign-reversing, monotone, zero-calibrated doubled trace). For every ratio orbit $q$, the doubled-trace real display of $F$ at the rational of $q$ equals the real display of the carrier-valued doubled trace of $F$ at $q$.
background
In the real-character factorization of the native cost, ratio orbits are the discrete carriers: an integer numerator over a nonzero distinction-denominator (K4.7). The doubled trace of a map $F$ on those orbits is turned into a real by traceDisplay: cast the doubled-trace value's rational to $\mathbb{R}$.
Separately, rationalTrace is the honest function on rational displays: send $x\in\mathbb{Q}$ to the orbit of $x$, then apply traceDisplay. The two presentations must agree when the rational is exactly $q$'s display, or later identities that mix orbit and rational language will not line up.
The hypothesis pack SansAnchorHypotheses is the anchor-free structural native-cost package: base without two, sign-reversing, monotone, and zero-calibrated doubled trace. Upstream, traceDisplay_eq_of_crossEq says the real display depends only on the cross-equality class of the orbit; K4.10 equates cross-equality with equality of rational displays.
proof idea
Term-mode reduction in two steps. Apply traceDisplay_eq_of_crossEq at the given $F$-hypotheses, which reduces the goal to cross-equality of $q$ with the orbit reconstructed from $q$'s rational. Rewrite that goal by crossEq_iff_toRat_eq (cross-equality iff equal rationals) and the recovery identity ratioOrbitOfRat_toRat, which says reconstructing an orbit from its rational and reading the rational back yields the original display. No further cost algebra is needed.
why it matters
This is the bridge between orbit-native and rational-native cost language inside real character factorization. Downstream, cost_display in GaugeOrbitClassification rewrites through it to identify the cost display with half the rational doubled trace minus one: the standard passage from doubled trace to the $J$-shaped cost. The sibling realCharacterCandidate_trace_of_pos works on the orbit display side of the same identity when building the real character candidate $x+x^{-1}$.
In the broader Recognition chain this supports uniqueness of the native cost and the real factorization that recovers the T5 $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) from structural hypotheses, without re-anchoring the base. It is bookkeeping, but the kind that lets gauge-orbit classification and character factorization share one doubled-trace object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.