rationalTrace_one
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the rational doubled-trace display evaluates to 2 at the unit rational. Cost and character-factorization arguments cite this as the unit normalization of the real-valued trace. The proof is a short calc: unfold the rational display, transport across the orbit of 1 via cross-equality, then apply the unit case of the carrier display.
Claim. Let $F$ map ratio orbits to ratio orbits and satisfy the anchor-free native-cost pack (base without two, sign-reversing, monotone, and zero-calibrated doubled trace). Then the rational doubled-trace display of $F$ at $1$ equals $2$: $\mathrm{Tr}_{\mathbb{Q}}(F)(1)=2$.
background
In the real character factorization of native cost, ratio orbits are the carrier for signed rational displays. The doubled trace of a map $F$ on those orbits is first valued in the carrier, then projected to a real via traceDisplay: cast the doubled-trace value to a rational and then to $\mathbb{R}$.
rationalTrace is the honest function on ordinary rationals obtained by sending $x\in\mathbb{Q}$ to its ratio-orbit representative and applying that real display. The hypothesis pack SansAnchorHypotheses is the anchor-free structural pack matching the PRC native-cost hypotheses without an external anchor: base without two, sign-reversing, monotone, and zero-calibrated doubled trace.
Upstream, traceDisplay_one already gives display value $2$ at the unit orbit, and traceDisplay_eq_of_crossEq says the real display is invariant under cross-equality of orbits. Cross-equality is equivalent to equality of rational verifier displays (crossEq_iff_toRat_eq).
proof idea
Short calc with two steps. First rewrite rationalTrace F 1 as traceDisplay F of the orbit of $1$, then apply traceDisplay_eq_of_crossEq under the anchor-free pack: the needed cross-equality is crossEq_iff_toRat_eq plus the fact that the orbit-of-rational round-trip and one_toRat both display as $1$. Second step is the one-line appeal to traceDisplay_one, which evaluates the carrier display at the unit orbit to $2$.
why it matters
Unit normalization of the rational doubled trace is the base case for extracting nontrivial real characters from native cost. Downstream, nontrivialCharacterValue_one feeds this equality into linear extraction at the unit to get character value $1$. nontrivialCharacterValue_two uses the same unit fact inside the d'Alembert/recurrence setup that identifies the value at $2$ with the anchor root. rationalTrace_two_pow_eq_two uses the companion normalization at $2$ and inducts along powers of two; the unit case anchors the trivial branch of that dichotomy.
In the Recognition cost story this is the real-display shadow of the doubled J-trace at the multiplicative unit: the cost character is forced to sit at the neutral value $2$ when the argument is $1$, consistent with the RCL/d'Alembert structure that later isolates $\phi$ and the unique native cost. It is a proved lemma inside the Cost domain, not scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.