nontrivialCharacterValue_two
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, if the rational trace at 2 is nondegenerate ($T_F(2)\neq 2$), the symbolic character extraction at the integer 2 recovers exactly the principal anchor root $r_F$. Anyone normalizing the real multiplicative character on positive integers cites this identity. The proof is pure algebra: d'Alembert at $(2,2)$ yields $T_F(4)=T_F(2)^2-2$, the root-sum identity rewrites $T_F(2)$, and the linear-extraction formula collapses by field arithmetic.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost pack (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). Write $T_F$ for its rational trace and $r_F$ for the principal real root of $T_F(2)$. If $T_F(2)\neq 2$, then the nondegenerate linear extraction evaluates at $2$ to the root itself: $\frac{r_F\,T_F(4)-T_F(2)}{r_F^2-1}=r_F$.
background
The module builds a real character factorization of native recognition cost on ratio orbits, without fixing an a-priori anchor. The structure SansAnchorHypotheses packages the anchor-free native-cost axioms: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace.
The rational trace $T_F:\mathbb{Q}\to\mathbb{R}$ records the cost display on rational points of the orbit. It obeys a d'Alembert (cosine-type) addition law under those hypotheses. The anchor root $r_F$ is the principal real root of the quadratic fixed by $T_F(2)$, so $r_F+r_F^{-1}=T_F(2)$ with $r_F\ge 1$. Nondegeneracy $T_F(2)\neq 2$ forces $r_F>1$, hence $r_F^2-1\neq 0$.
The nontrivial character value is the linear extraction $\frac{r,T(2x)-T(x)}{r^2-1}$ with $r=r_F$ and $T=T_F$. It is designed to peel a pure multiplicative character off the doubled trace once the root is known.
proof idea
Apply the rational-trace d'Alembert identity at the pair $(2,2)$. After rewriting $2\cdot 2=4$ and $2/2=1$ and using $T_F(1)=2$ (zero-calibration), rearrange to $T_F(4)=T_F(2)^2-2$.
Invoke $r_F\neq 0$ and $r_F^2-1\neq 0$ (the latter from nondegeneracy). Rewrite $T_F(2)=(r_F^2+1)/r_F$ via the root-sum identity $r_F+r_F^{-1}=T_F(2)$.
Unfold the definitions of nontrivial character value and linear extraction at $x=2$, substitute the two identities above, and finish by field_simp plus ring.
why it matters
This pins the character extraction at the distinguished integer 2 to the geometric anchor root itself. Downstream, exists_nat_exponent (GaugeOrbitClassification) quotes it as the base case that turns Howe's real exponent into a positive integer power: once the value at 2 is $r_F$, six-exponentials input forces the exponent on all naturals to be a natural number. The sibling nontrivialCharacterValue_principal_on_nat likewise starts from this equality to prove positivity on $\mathbb{N}$.
In the Recognition framework the construction sits inside the cost layer that realizes J-uniqueness (forcing step T5): the native cost is forced to the hyperbolic cosine shape, and the character factorization separates the multiplicative orbit data from the J-display. Closing the integer-exponent step is what lets gauge orbits be classified by a single natural power of the anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.