realTraceRoot_pos
plain-language theorem explainer
For every real t ≥ 2, the principal root of X² − tX + 1 = 0 is strictly positive. Anyone clearing inverses in the real-trace or d'Alembert identities cites this. The proof is a one-line chain: 0 < 1 ≤ root, via the already-proved lower bound of one.
Claim. For every real number $t \ge 2$, the principal root $\dfrac{t + \sqrt{t^2 - 4}}{2}$ of the quadratic $X^2 - t X + 1 = 0$ satisfies $0 < \dfrac{t + \sqrt{t^2 - 4}}{2}$.
background
In the real-trace root module, realTraceRoot t is defined as the principal (at least one) root of the monic reciprocal quadratic $X^2 - t X + 1 = 0$, namely $(t + \sqrt{t^2 - 4})/2$, for parameters $t \ge 2$. Reciprocal quadratics of this shape arise whenever a positive real and its inverse appear as a conjugate pair with fixed sum $t$; the sum is the trace of the corresponding $2 \times 2$ companion matrix.
The sibling lemma realTraceRoot_ge_one already shows that this root is at least one whenever $t \ge 2$. Positivity is the strictly weaker statement needed to form the multiplicative inverse without a zero-denominator side condition. The local setting is pure real analysis supporting the Recognition cost calculus (J-cost and multiplicative d'Alembert identities), not yet the full forcing chain.
proof idea
One-line wrapper. Apply the Mathlib comparison lt_of_lt_of_le to the pair $0 < 1$ (zero_lt_one) and the already-proved bound $1 \le \mathrm{realTraceRoot}, t$ (realTraceRoot_ge_one under the hypothesis $t \ge 2$). No unfolding of the square-root definition is required.
why it matters
The immediate consumer is realTraceRoot_add_inv, which proves that the root plus its inverse recovers the trace parameter $t$. That identity opens with ne_of_gt (realTraceRoot_pos ht) to justify writing the inverse. Downstream multiplicative lemmas (realTraceRoot_mul, the d'Alembert product and difference-of-squares identities) inherit the same non-vanishing fact.
In the Recognition cost layer these reciprocal roots encode the self-dual pairs that appear in the Recognition Composition Law and in closed-form evaluations of the J-cost along geometric progressions. The positivity lemma is elementary scaffolding, but without it the inverse-sum identity and the subsequent multiplicative structure cannot even be stated in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.