traceDisplay_eq_of_crossEq
plain-language theorem explainer
Cross-equivalent ratio orbits yield the same real doubled-trace display under any anchor-free native cost map F. Cost theorists cite it to treat the display as a well-defined function of the rational class rather than a particular orbit representative. The argument normalizes both orbits, transports the doubled-trace congruence, and casts the resulting cross-equality to real equality.
Claim. Let $F$ map ratio orbits to ratio orbits and satisfy the anchor-free native-cost hypotheses (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). If two ratio orbits $q$ and $r$ are cross-equivalent (cross-multiplication balances as signed orbits), then the real display of the doubled trace agrees: $\mathrm{tr}_F(q)=\mathrm{tr}_F(r)\in\mathbb{R}$.
background
In the Primitive Recognition Calculus, rationals are carried by ratio orbits: pairs of signed distinction orbits with a nonzero denominator. Two orbits are cross-equivalent when $a.num\cdot b.den$ balances $b.num\cdot a.den$ as signed orbits; by K4.10 this is equivalent to equality of the verifier rational displays $a.toRat=b.toRat$.
The doubled trace of a native cost map $F$ is a carrier-valued object on ratio orbits. Its real display traceDisplay casts that carrier value through the rational bridge to $\mathbb{R}$. The structure SansAnchorHypotheses packages the anchor-free structural assumptions on $F$: a base-sans-two pack, sign-reversal, monotonicity, and zero-calibration of the doubled trace.
This module builds a real character factorization of native cost. Well-definedness of the display on cross-classes is the bridge from orbit-level data to a genuine function of rational arguments.
proof idea
Apply the base-sans-two normalized-invariance of $F$ at $q$ and at $r$, then pass each through doubledTraceValue_congr to obtain cross-equalities between the doubled traces and the traces of the normalized orbits.
Invoke PRCNormalizeRatioCanonicalTarget_proved on the given cross-equality $q\sim r$ to identify the two normalized targets. Rewrite the $q$-side congruence along that identity, then chain with the symmetric $r$-side congruence via crossEq_trans and crossEq_symm.
Convert the resulting cross-equality to rational equality by crossEq_iff_toRat_eq. Unfold traceDisplay and nativeCostDoubledTrace, and close by exact_mod_cast.
why it matters
Without invariance under cross-equivalence, the doubled trace cannot descend to a function of rationals. This lemma is the well-definedness step that lets rationalTrace be defined on $\mathbb{Q}^{\times}$ and compared to the orbit display.
Downstream it is applied directly in rationalTrace_eq_traceDisplay (display agrees with the rationalized trace), then in the calibration identities rationalTrace_one and rationalTrace_recip, and finally in rationalTrace_dAlembert, which establishes the d'Alembert functional equation on nonzero rationals. That equation is the rational shadow of the Recognition Composition Law and feeds the uniqueness path toward the J-cost $J(x)=(x+x^{-1})/2-1$ (forcing step T5).
In short: it closes the orbit-to-rational gap so the native cost character can be treated as a real multiplicative functional on $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.