cost_display
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the real display of cost at any ratio orbit equals half the rational doubled-trace minus one. Gauge-orbit classification and the PRC recognizer bridge cite this to move between cost and trace language. The proof rewrites through the trace-display equality, unfolds the doubled-trace definition, and finishes by ring arithmetic.
Claim. Let $F$ satisfy the anchor-free native-cost hypotheses (base without two, sign-reversing, monotone, and zero-calibrated doubled trace). For every ratio orbit $q$, $((F q).\mathrm{toRat}:\mathbb{R}) = \frac{1}{2}\,T_{\mathbb{Q}}(F,q)-1$, where $T_{\mathbb{Q}}$ is the doubled-trace display evaluated on the rational representative of $q$.
background
In the cost module, native cost is a map $F$ on ratio orbits. The doubled trace packages the symmetric combination that becomes the classical $J$-cost after halving and shifting: $J(x)=(x+x^{-1})/2-1$. The real display of that carrier-valued doubled trace is traceDisplay; rationalTrace is the same quantity viewed as a function of rational displays.
SansAnchorHypotheses is the anchor-free pack: base without two, sign-reversing, monotone, and zero-calibrated doubled trace. It matches the structural native-cost hypotheses used by the primitive recognition calculus, without fixing an absolute scale anchor.
Upstream, rationalTrace_eq_traceDisplay identifies the rational-trace evaluation at $q.\mathrm{toRat}$ with traceDisplay at $q$, once the anchor-free pack holds. That identification is the only nontrivial lemma this identity needs before pure arithmetic.
proof idea
Term-mode proof in four steps. First rewrite the right-hand side via rationalTrace_eq_traceDisplay, replacing rational-trace-at-$q.\mathrm{toRat}$ by traceDisplay F q. Then simp only unfolds traceDisplay, nativeCostDoubledTrace, and doubledTraceValue, together with the toRat lemmas for multiplication, addition, two, and one on ratio orbits. push_cast moves the remaining casts into $\mathbb{R}$. A final ring closes the identity $(t/2)-1$ against the unfolded cost display.
why it matters
This is the local dictionary between cost display and doubled-trace display. Downstream, cost_at_pos uses it to identify positive-display cost with $J$ of a $k$-th power; degenerate_is_signGauge and both vanishes_at_two_iff_* theorems convert vanishing cost at orbit two into the degenerate-trace condition and flatness on all positive ratios; charges_positively_at_two reads nondegeneracy as a strict inequality. The PRC recognizer bridge certificate also records the same display identity as part of the recognition-cost surface. In framework terms it is the concrete realization of T5 $J$-uniqueness on ratio orbits: cost is the halved-and-shifted trace, not an independent functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.