nontrivialCharacterValue_nonzero
plain-language theorem explainer
Under the anchor-free native-cost pack, if the doubled rational trace at 2 is nondegenerate (not equal to 2), the extracted real character value on every nonzero rational is nonzero. Used when proving positivity on naturals and nondegeneracy of the real character candidate. Proof is a short contradiction from multiplicativity plus the unit value at 1.
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). Suppose the rational doubled trace of $F$ at $2$ is not $2$. Then for every nonzero rational $x$, the nontrivial character value of $F$ at $x$ is nonzero.
background
In Cost.RealCharacterFactorization, native cost data on ratio orbits is converted into a real multiplicative character via the doubled trace. The rational trace is the doubled trace read on rational displays: $\mathrm{rationalTrace},F,x$ is the trace display of $F$ on the orbit of $x\in\mathbb{Q}$.
The nontrivial character value is the nondegenerate symbolic extraction of that trace at the anchor root: a linear extraction of $\mathrm{rationalTrace},F$ against $\mathrm{anchorRoot},F$. Degeneracy is detected by the single numerical test $\mathrm{rationalTrace},F,2=2$; the complementary hypothesis keeps the extraction away from the trivial character.
SansAnchorHypotheses packages the anchor-free structural pack matching PRCStructuralNativeCostHypothesesSansAnchor: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Multiplicativity and the unit value at $1$ are already available under those hypotheses plus nondegeneracy.
proof idea
Term-mode contradiction from the multiplicative structure. Apply nontrivialCharacterValue_mul to $x$ and $x^{-1}$ (both nonzero). Rewrite the product $x\cdot x^{-1}$ to $1$ and replace the left-hand side by nontrivialCharacterValue_one, obtaining
$$1=\mathrm{nontrivialCharacterValue},F,x\cdot\mathrm{nontrivialCharacterValue},F,x^{-1}.$$
Assume the first factor is zero; zero_mul collapses the right-hand side to $0$, and norm_num yields $1=0$.
why it matters
Nonvanishing is the gate before positivity and before the real character candidate can be treated as a genuine character. Downstream, nontrivialCharacterValue_pos_on_nat uses it (with the natural embedding nonzero) to get strict positivity on $\mathbb{N}_{\ge 1}$, and realCharacterCandidate_nonzero cases on the degeneracy test and invokes this lemma on the nondegenerate branch.
In the Recognition cost stack this sits under real-character factorization of native cost: the J-cost / RCL lineage forces a unique cost shape, and the character extraction turns the doubled trace into a multiplicative real map on ratio orbits. Without nonvanishing, the candidate would collapse on a dense set and could not feed later uniqueness or mass-ladder comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.