realCharacterCandidate_nonzero
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the real character candidate extracted from the doubled trace never vanishes on nonzero rational orbits. Cost and character theorists cite it when assembling the PRC real-ratio character package. The proof is a two-branch case split on whether the doubled trace at 2 is degenerate, dispatching each branch to an existing nonvanishing lemma.
Claim. Let $F$ be a map on rational orbits satisfying the anchor-free native-cost hypotheses (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). For every rational orbit $x$ with rational display $x\neq 0$, the real character candidate built from the doubled trace of $F$ satisfies $\chi_F(x)\neq 0$.
background
In the real-character factorization module, native cost data on rational orbits are packaged without a fixed anchor. The structure SansAnchorHypotheses collects four properties: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace, matching the structural PRC native-cost pack without an anchor point.
The doubled trace is exposed on rational displays by rationalTrace F x. From it one extracts a real-valued candidate character: if rationalTrace F 2 = 2 (the degenerate anchor), the candidate is the ordinary rational sign character; otherwise it is the nontrivial generalized linear extraction (with value 0 only at the zero display).
Ratio orbits are the K4.7 displays: integer numerator over a nonzero distinction-nat denominator, with a map to rationals. Nonvanishing of the candidate on nonzero orbits is the gate that lets the candidate enter the PRC real-ratio character interface.
proof idea
Case-split on whether rationalTrace F 2 = 2.
Degenerate branch: the candidate reduces by definition to the rational sign character on x.toRat. Apply rationalSignCharacter_nonzero at the hypothesis x.toRat ≠ 0.
Nondegenerate branch: the candidate reduces to the nontrivial character value. Apply nontrivialCharacterValue_nonzero with the anchor-free pack, the inequality rationalTrace F 2 ≠ 2, and x.toRat ≠ 0.
Both branches are one-line simp reductions of the candidate definition followed by the matching upstream nonvanishing lemma.
why it matters
This lemma is a structural ingredient of realCharacterCandidate_is_character, which packages the candidate as a full PRC real-ratio character (unit, multiplicative, reciprocal). Without nonvanishing, the character interface cannot be inhabited.
In the Recognition cost layer, real characters factor the doubled-trace data that ultimately feed native-cost uniqueness and the J-cost story (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$, and the Recognition Composition Law). The result closes the zero-free gate on the character side of the factorization, so downstream cost-from-character constructions can treat $\chi_F$ as a genuine multiplicative character on nonzero rational orbits.
It is fully proved (no sorry); the only hypotheses are the anchor-free pack and nonzero display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.