realTraceRoot_ge_one
plain-language theorem explainer
For every real t at least 2, the principal root of X² − tX + 1 = 0 is at least 1. Cost and character-factorization arguments cite this to keep the larger hyperbolic root on the unit side of the reciprocal pair. The proof unfolds the closed form, uses nonnegativity of the square root, and finishes by linear arithmetic.
Claim. Let $t \in \mathbb{R}$ with $t \ge 2$. Write $r(t) = \frac{t + \sqrt{t^2 - 4}}{2}$ for the principal root of $X^2 - tX + 1 = 0$. Then $1 \le r(t)$.
background
In the real-trace cost layer, each admissible trace parameter $t \ge 2$ labels the monic reciprocal quadratic $X^2 - tX + 1 = 0$. Its two roots multiply to 1; the principal branch is defined by
$$r(t) = \frac{t + \sqrt{t^2 - 4}}{2}.$$
The companion root is $1/r(t)$. The definition is stated only for $t \ge 2$ so that the discriminant is nonnegative and $r(t)$ is real. This is the same algebraic object that appears as the larger eigenvalue of a $2 \times 2$ unimodular matrix with trace $t$, and later as the anchor root of a ratio-orbit character.
proof idea
Unfold $r(t)$ to $(t + \sqrt{t^2-4})/2$. Nonnegativity of the real square root gives $\sqrt{t^2-4} \ge 0$. Combined with the hypothesis $t \ge 2$, linear arithmetic yields $t + \sqrt{t^2-4} \ge 2$, hence $r(t) \ge 1$. No external lemmas beyond Real.sqrt_nonneg are required.
why it matters
The bound is the elementary gate that keeps the principal root on the side $\ge 1$ of the reciprocal pair. Downstream, realTraceRoot_pos obtains strict positivity by chaining $0 < 1 \le r(t)$. In the character-factorization module, anchorRoot_ge_one reduces the same inequality for the anchor root of a ratio-orbit map to this lemma once the display trace is known to be at least 2. Within Recognition Science cost calculus, that positivity and ordering underwrite multiplicative identities (d'Alembert-type product and difference-of-squares formulae) used when factoring real characters along the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.