anchorRoot_sq_sub_one_ne_zero
plain-language theorem explainer
Under anchor-free native-cost hypotheses, if the doubled trace at 2 is not the trivial value 2, then the squared principal root extracted from that trace differs from 1. Character-factorization proofs cite this to keep the linear extraction denominator nonzero. The argument is a one-line comparison: the root is strictly greater than 1, so nlinarith finishes.
Claim. Let $F$ map rational orbits to rational orbits and satisfy the anchor-free native-cost pack (base without two, sign-reversing, monotone, zero-calibrated doubled trace). If the rational doubled trace of $F$ at $2$ is not equal to $2$, then writing $r$ for the principal real root of that trace value one has $r^2 - 1 \neq 0$.
background
In the real character factorization of native cost, one works with maps $F$ on ratio orbits (integer numerator over nonzero orbit denominator). The pack SansAnchorHypotheses collects the structural native-cost axioms without fixing an anchor: base without two, sign-reversing, monotone, and zero-calibrated doubled trace.
The rational doubled trace sends a rational display $x$ to the real trace of $F$ on the corresponding orbit. The anchor root is the principal real root of that trace evaluated at the distinguished integer two: $r = \mathrm{realTraceRoot}(\mathrm{rationalTrace}, F, 2)$.
Upstream, anchorRoot_gt_one already gives $1 < r$ whenever the same hypotheses hold and the trace at two is nontrivial ($\mathrm{rationalTrace}, F, 2 \neq 2$). That strict inequality is the only input needed here.
proof idea
Obtain $1 < \mathrm{anchorRoot}, F$ from anchorRoot_gt_one under the same pack and nontriviality hypothesis. Then nlinarith closes $r^2 - 1 \neq 0$ from the strict lower bound $r > 1$. No further cost identities are invoked.
why it matters
This is a small but mandatory nondegeneracy gate for the nontrivial real character extracted from the doubled trace. Downstream, nontrivialCharacterValue_one feeds it (with anchorRoot_ne_zero and anchorRoot_add_inv) into the unit case of linear extraction; nontrivialCharacterValue_mul, nontrivialCharacterValue_recip_sum, and nontrivialCharacterValue_two rely on the same character value being well-defined and multiplicative.
In the Recognition cost story this keeps the factorization of the native cost away from the trivial character (trace at two equal to 2). It sits inside the real-character side of J-cost uniqueness (T5 / RCL), ensuring the principal root used as the character generator is not $\pm 1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.