anchorRoot_ne_zero
plain-language theorem explainer
Under the anchor-free native-cost hypotheses on a ratio-orbit map F, the principal real root extracted from the doubled trace at two is strictly nonzero. Anyone building the real multiplicative character from the cost trace cites this to justify division and reciprocal identities. The proof is a one-line wrapper: positivity of one plus the already-proved lower bound one forces the root above zero.
Claim. Let $F$ be a map on rational orbits satisfying the anchor-free native-cost package (base law away from two, sign-reversal, monotonicity, and zero-calibrated doubled trace). Then the principal real root of the rational trace of $F$ at two is nonzero: $\mathrm{anchorRoot}(F) \neq 0$.
background
In the real character factorization of native cost, one extracts a real multiplicative character from the doubled trace of a ratio-orbit map $F$. The distinguished sample point is the positive integer two: the rational trace at two is turned into a principal real root via realTraceRoot, called the anchor root.
The hypothesis pack SansAnchorHypotheses is the anchor-free structural package matching the PRC native-cost axioms without a fixed anchor: base law away from two, sign-reversing cost, monotonicity, and zero-calibrated doubled trace. Upstream, anchorRoot_ge_one already shows that under this pack the anchor root is at least one, by reducing to the display inequality that the trace at two is at least two and applying the root lower bound.
Ratio orbits are the K4.7 rational displays (signed numerator over nonzero distinction denominator) on which native cost acts. The present lemma only needs the positivity side of that geometry.
proof idea
One-line wrapper. From anchorRoot_ge_one hF one has $1 \le \mathrm{anchorRoot}(F)$. Chain with $0 < 1$ via lt_of_lt_of_le to obtain $0 < \mathrm{anchorRoot}(F)$, then apply ne_of_gt to conclude nonzero. No new analysis of the trace or root extraction is performed.
why it matters
Nonvanishing of the anchor root is the gate for the nontrivial real character value. Downstream, nontrivialCharacterValue_one invokes it (with the unit extraction lemma) to get character value one at one; nontrivialCharacterValue_mul, nontrivialCharacterValue_recip_sum, and nontrivialCharacterValue_two all sit on the same nondegeneracy so that products, reciprocal sums, and the identification of the value at two with the anchor root are well-defined.
In the Recognition cost story this is the real-side counterpart of keeping the J-cost character away from the trivial fixed point: the root at two is the seed of the multiplicative factorization that recovers the cost display. It does not itself force the T5 J-uniqueness or the RCL identity, but it clears the algebraic path those identities use once the character is assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.