traceDisplay
plain-language theorem explainer
Maps a native cost F and a ratio orbit q to the real number obtained by reading the carrier-valued doubled trace as a rational, then casting to ℝ. Anyone working with real-valued cost displays, d'Alembert identities on ℚ, or gauge-orbit classification cites this. The body is a two-step transport: nativeCostDoubledTrace then toRat, cast to ℝ.
Claim. Given a map $F$ on ratio orbits and a ratio orbit $q$, the real display of the doubled trace is $\mathrm{traceDisplay}(F,q) := \bigl(T_F(q)\bigr)_{\mathbb{Q}} \in \mathbb{R}$, where $T_F(q) = 2\bigl(F(q)+1\bigr)$ is the carrier-valued doubled d'Alembert trace and $(\cdot)_{\mathbb{Q}}$ is the verifier rational display of a ratio orbit.
background
In the Primitive Recognition Calculus, costs act on ratio orbits: structures with integer numerator and nonzero distinction-nat denominator. The verifier map toRat sends such an orbit to $\mathbb{Q}$ by ordinary division of the integer displays (spec tag A5: transport wrapper, internal law is cross-multiplication).
The doubled d'Alembert trace of a native cost $F$ is the carrier-valued quantity $T_F(q)=2(F(q)+1)$. For a generated cost this equals $\chi(q)+\chi(q)^{-1}$. The present definition simply exports that carrier value into $\mathbb{R}$ via the rational display.
The module RealCharacterFactorization builds the real character factorization of native costs without an anchor hypothesis package at every step; this display is the bridge from orbit-level arithmetic to ordinary real analysis on $\mathbb{Q}$.
proof idea
Pure definitional transport, not a proof. Compose nativeCostDoubledTrace F q (which is doubledTraceValue (F q)) with the ratio-orbit toRat, then coerce $\mathbb{Q}\to\mathbb{R}$. No lemmas are applied; the body is a single cast of that rational.
why it matters
This is the real-valued face of the doubled trace that every later rational-trace lemma quotes. Downstream, rationalTrace is defined as traceDisplay F on the orbit of a rational; rationalTrace_eq_traceDisplay identifies the two under SansAnchor hypotheses; rationalTrace_dAlembert lifts the RCL-style identity $T(xy)+T(x/y)=T(x)T(y)$ to $\mathbb{Q}$; and cost_display in GaugeOrbitClassification recovers the cost itself as half the trace display minus one.
In the Recognition framework the doubled trace is the concrete d'Alembert character attached to the unique J-cost (forcing chain T5: $J(x)=(x+x^{-1})/2-1$). Exporting it to $\mathbb{R}$ is what lets gauge-orbit classification and sign-gauge checks (e.g. degenerate value 2 at the anchor) speak ordinary real numbers rather than carrier orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.