nontrivialCharacterValue_recip_sum
plain-language theorem explainer
Under anchor-free native-cost hypotheses on a ratio-orbit map F, if the doubled rational trace is nondegenerate at 2, the extracted nontrivial character at a nonzero rational and at its reciprocal sum to the rational trace. Cost theorists cite this when recovering the additive character from a d'Alembert-type trace. The proof is a direct specialization of the linear-extraction reciprocal-sum identity to the anchor root side conditions.
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). If the rational trace $T_F$ of $F$ at $2$ is not equal to $2$, then for every nonzero rational $x$, $\chi_F(x^{-1})+\chi_F(x)=T_F(x)$, where $\chi_F$ is the nontrivial character value extracted from $T_F$ via the anchor root of $F$.
background
In the real-character factorization of native cost, the doubled trace of a ratio-orbit map $F$ is reified as an honest function $T_F$ on rational displays (the rational trace). Under the anchor-free pack SansAnchorHypotheses (base without two, sign-reversing, monotone, and zero-calibrated doubled trace), one extracts a real anchor root $r_F$ from the value $T_F(2)$, normalized so that $r_F+(r_F)^{-1}=T_F(2)$.
When $T_F(2)\neq 2$ the situation is nondegenerate: $r_F>1$, so $r_F\neq 0$ and $r_F^2-1\neq 0$. The nontrivial character value $\chi_F(x)$ is then the linear extraction of $T_F$ at this anchor root. The rational trace itself obeys reciprocity $T_F(x^{-1})=T_F(x)$ and a d'Alembert identity $T_F(xy)+T_F(x/y)=T_F(x),T_F(y)$ on nonzero rationals, which is the algebraic content of the Recognition Composition Law at the level of traces.
proof idea
One-line wrapper that applies the private lemma linearExtraction_recip_sum to $T:=T_F$ and $r:=r_F$. The five side conditions are discharged by: reciprocity of the rational trace, the d'Alembert identity for the rational trace, nonvanishing of the anchor root, nonvanishing of $r_F^2-1$ (from nondegeneracy $T_F(2)\neq 2$), and the identity $r_F+(r_F)^{-1}=T_F(2)$. The nonzero hypothesis on $x$ is passed through unchanged.
why it matters
This identity is the reciprocal-sum half of the character reconstruction: it shows that the extracted $\chi_F$ is the additive piece whose sum with its reciprocal recovers the full rational trace. The immediate parent is nontrivialCharacterValue_trace, which upgrades the same data to $\chi_F(x)+(\chi_F(x))^{-1}$ equal to a normalized display of the trace, completing the factorization of the cost character on rationals.
In the Recognition framework this sits inside the cost layer that realizes the unique $J$-cost forced by T5 and the Recognition Composition Law. The nondegeneracy gate $T_F(2)\neq 2$ separates the trivial (constant-two) orbit from the genuine hyperbolic character that feeds the phi-ladder and the native mass/yardstick calculus. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.