nontrivialCharacterValue_trace
plain-language theorem explainer
Under anchor-free native-cost hypotheses, the nontrivial real character extracted from the doubled trace satisfies χ(x) + χ(x)⁻¹ = Tr(x) for every nonzero rational display x. Cost and gauge-orbit classification cite this identity to recover the J-cost shape from the character. The proof rewrites the reciprocal-sum lemma by the reciprocal law and closes by linear arithmetic.
Claim. Let $F$ be a map on rational orbits satisfying the anchor-free native-cost pack (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). If the rational doubled trace is nontrivial at $2$ ($\mathrm{Tr}_F(2)\neq 2$), then for every nonzero rational $x$, the nontrivial character value $\chi_F(x)$ obeys $\chi_F(x)+\chi_F(x)^{-1}=\mathrm{Tr}_F(x)$.
background
In the real-character factorization of native cost, the doubled trace is promoted to an honest function rationalTrace on rational displays: evaluate the orbit map $F$ on the ratio-orbit of $x$ and read the display trace. The nontrivial character value is the nondegenerate linear extraction of that trace against the anchor root at two; it is the symbolic real character candidate once $\mathrm{Tr}_F(2)\neq 2$.
SansAnchorHypotheses packages the anchor-free structural pack matching PRC native-cost hypotheses without a fixed anchor: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Ratio orbits are K4.7 rational displays (signed numerator over nonzero distinction denominator).
Upstream, the reciprocal-sum identity already gives $\chi(x^{-1})+\chi(x)=\mathrm{Tr}(x)$, and the reciprocal law gives $\chi(x^{-1})=\chi(x)^{-1}$. The present statement is the standard character-trace form $\chi+\chi^{-1}=\mathrm{Tr}$ used throughout cost factorization and gauge-orbit work.
proof idea
Term-mode reduction in three steps. Invoke nontrivialCharacterValue_recip_sum to obtain $\chi(x^{-1})+\chi(x)=\mathrm{Tr}_F(x)$. Rewrite the first summand via nontrivialCharacterValue_recip, which replaces $\chi(x^{-1})$ by $\chi(x)^{-1}$. Close with linarith to rearrange into $\chi(x)+\chi(x)^{-1}=\mathrm{Tr}_F(x)$. No new analysis: pure algebraic transport of the two reciprocal lemmas.
why it matters
This is the bridge from extracted real characters to the classical J-shape of Recognition cost. Downstream, cost_at_pos in GaugeOrbitClassification uses it (via character-at-positive) so that on a positive display the cost is $J$ of the $k$-th power. exists_nat_exponent relies on the same character package to force a positive integer exponent (Howe plus six-exponentials). In-module, positivity on naturals, nat-trace monotonicity, and realCharacterCandidate_trace_of_pos all quote this identity.
Framework-wise it realizes the T5 J-uniqueness link: once $\chi+\chi^{-1}$ equals the doubled trace, the cost is forced into the $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh\log x-1$) family compatible with the Recognition Composition Law. It is proved, not scaffolding; it closes the algebraic half of the real-character factorization before gauge classification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.