nontrivialCharacterValue_recip
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the nontrivial character extracted from the doubled trace is reciprocal: its value at the inverse of a nonzero rational equals the inverse of its value. Anyone proving the trace identity χ+χ⁻¹ or classifying real characters on ratio orbits cites this. The argument is a short algebraic consequence of multiplicativity plus the unit value at 1.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base without two, sign-reversing, monotone, zero-calibrated doubled trace). Suppose the rational doubled trace of $F$ at $2$ is not $2$. Then for every nonzero rational $x$, $\chi_F(x^{-1})=\chi_F(x)^{-1}$, where $\chi_F$ is the nontrivial character value obtained by linear extraction of the rational trace against the anchor root of $F$.
background
The module factors native cost maps on ratio orbits into real characters. A ratio orbit is an integer-numerator over nonzero orbit-denominator display of a rational (K4.7). The rational trace is the doubled trace of $F$ read on the orbit of a rational display.
SansAnchorHypotheses is the anchor-free pack matching the structural native-cost hypotheses: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. The nontrivial character value is the nondegenerate symbolic extraction from the trace at two: linear extraction of the rational trace against the anchor root. Nontriviality (rational trace at $2$ unequal to $2$) keeps that extraction nondegenerate.
Upstream, multiplicativity of the character on nonzero rationals and the unit identity $\chi_F(1)=1$ are already proved under the same pack.
proof idea
Instantiate multiplicativity on the pair $(x,x^{-1})$ to get $\chi_F(x\cdot x^{-1})=\chi_F(x),\chi_F(x^{-1})$. Rewrite the product to $1$ and apply the unit lemma $\chi_F(1)=1$, so $1=\chi_F(x),\chi_F(x^{-1})$. Finish by the field fact that a right multiplicative inverse of one is the reciprocal. Term-mode, three steps, no new analysis.
why it matters
Closes the reciprocal half of the multiplicative character package. Downstream it is used by the trace identity $\chi_F(x)+\chi_F(x)^{-1}$ (the doubled-trace reconstruction), by the reciprocal law for the real character candidate on ratio orbits, and by the gauge-orbit classification theorem that extends power-law character values from the naturals to every positive rational.
In the Recognition framework this matches the $J(x)+J(x^{-1})$ structure of the Recognition Composition Law and the T5 $J$-uniqueness form $\cosh(\log x)-1$. Without reciprocity, native-cost factorization into a real character cannot close under inversion of displays, and the power-law classification on positive rationals stalls.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.