anchorRoot_gt_one
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, if the doubled trace at two is not the degenerate value 2, the principal real root extracted from that trace is strictly larger than 1. Cost and gauge-orbit arguments cite this to guarantee a nontrivial positive base for character powers. The proof upgrades the weak inequality 1 ≤ root by a one-line contradiction with the add-inverse identity.
Claim. Let $F$ be a map on rational orbits satisfying the anchor-free native-cost pack (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). If the rational doubled trace of $F$ at $2$ is not equal to $2$, then the principal real root of that trace value satisfies $1 < r_F$.
background
In the real-character factorization of native cost, one extracts a real scalar from the doubled trace evaluated at the distinguished positive integer two. The rational doubled trace rationalTrace F x is the real display of the native doubled-trace functional on the ratio-orbit of the rational $x$. The principal root anchorRoot F is defined as the real-trace root of that value at two: the unique $r \ge 1$ with $r + r^{-1}$ equal to the trace display.
The ambient hypotheses are the anchor-free pack matching the structural native-cost axioms without a fixed anchor: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Under those axioms one already has the weak bound $1 \le$ anchor root and the identity anchor root plus its inverse equals the rational trace at two.
The nontriviality hypothesis rationalTrace F 2 ≠ 2 rules out the degenerate fixed point of that identity (where the root would be exactly 1).
proof idea
Start from the already-proved weak bound anchorRoot_ge_one, which gives $1 \le$ anchor root. It remains only to exclude equality. Assume the root equals 1. Substitute into anchorRoot_add_inv to obtain $1 + 1^{-1} =$ rational trace at 2. Numerical simplification yields rational trace at 2 equal to 2, contradicting the nontriviality hypothesis. Hence the inequality is strict. The argument is a short lt_of_le_of_ne refinement; no new analysis is required beyond the two upstream root lemmas.
why it matters
Strict positivity of the anchor root above 1 is the gate that turns a real multiplicative character into a genuine power base. Downstream, exists_nat_exponent in GaugeOrbitClassification uses it (with Howe and the six-exponentials input) to force the character exponent on natural numbers to be a positive integer: "Howe supplies the real exponent, the anchor root makes it positive, and the six exponentials input makes it an integer." Locally it feeds anchorRoot_sq_sub_one_ne_zero (so $r^2 - 1 \ne 0$) and nontrivialCharacterValue_principal_on_nat (so character values on naturals stay at least 1).
In the Recognition cost story this is the nondegeneracy step that keeps the real factorization of the native cost away from the trivial J-character. It sits under the uniqueness chain for the PRC native cost and supports the later gauge-orbit classification of multiplicative characters on ratio orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.