realTraceRoot_sq_sub_four_nonneg
plain-language theorem explainer
If a real number t satisfies t ≥ 2, then t² − 4 is nonnegative. Anyone constructing the principal real branch of the inverse of x ↦ x + x⁻¹ (the trace root) cites this to justify √(t² − 4). The proof is a one-line nonlinear arithmetic check.
Claim. For every real number $t$ with $t \ge 2$, one has $t^2 - 4 \ge 0$.
background
The module develops the real principal branch of the inverse of the trace map $x \mapsto x + x^{-1}$ on $(0,\infty)$. For $t \ge 2$ that inverse is realized by
$$\mathrm{realTraceRoot}(t) = \frac{t + \sqrt{t^2-4}}{2},$$
the larger root of $x + x^{-1} = t$. The radicand $t^2-4$ must be shown nonnegative before any appeal to Real.sqrt or Real.sq_sqrt is legal.
This inequality is the elementary gate for every subsequent identity in the file: the reconstruction $r + r^{-1} = t$, the product formula for principal branches, and the cosh-style addition formula that recovers the larger summand from a sum and a squared difference.
proof idea
One-line tactic proof: nlinarith discharges $t \ge 2 \Rightarrow t^2 - 4 \ge 0$ from the ordered-field axioms and the square of a nonnegative quantity. No named lemmas are invoked.
why it matters
The lemma is the nonnegativity certificate used by three downstream results in the same module: realTraceRoot_add_inv (which needs Real.sq_sqrt on $t^2-4$), realTraceRoot_mul (multiplication of principal branches, the algebraic form of cosh addition), and larger_trace_of_diff_sq (recovering the larger trace from a sum and a squared difference).
Those identities equip the cost side of Recognition Science with a real multiplicative structure compatible with the J-cost $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law. They sit under the T5 uniqueness of $J$ and the hyperbolic parametrization that later feeds the eight-tick and dimension-forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.