realTraceRoot_one
plain-language theorem explainer
The principal real root of X² − 2X + 1 = 0 equals 1. Anyone normalizing the trace-root map at the boundary trace t = 2 cites this evaluation. The proof is a one-line simplification of the closed form using √0 = 0.
Claim. The principal root of $X^2 - t X + 1 = 0$ evaluated at $t = 2$ equals $1$: $\frac{2 + \sqrt{2^2 - 4}}{2} = 1$.
background
In Cost.RealTraceRoot, the map sending a real trace $t \ge 2$ to its principal root is defined by $$\mathrm{realTraceRoot}(t) = \frac{t + \sqrt{t^2 - 4}}{2}.$$ By construction this is the unique root $\ge 1$ of the reciprocal quadratic $X^2 - t X + 1 = 0$ (the larger eigenvalue of an SL(2)-type matrix with that trace).
The boundary value $t = 2$ is the double-root case: the discriminant vanishes and both roots collapse to $X = 1$. That point is the neutral element for the multiplicative structure developed by the sibling lemmas (add-inverse, product, and d'Alembert identities) in the same module. In Recognition Science it matches the unique zero of the J-cost $J(x) = (x + x^{-1})/2 - 1$.
proof idea
One-line wrapper via simp. Unfold the closed-form definition, discharge $2^2 - 4 = 0$ by norm_num, rewrite Real.sqrt 0 = 0, and the arithmetic $(2 + 0)/2 = 1$ finishes.
why it matters
Supplies the unit evaluation of the principal trace-root map that underpins the whole Cost.RealTraceRoot development. Sibling results (realTraceRoot_ge_one, realTraceRoot_add_inv, realTraceRoot_mul, and the mulDAlembert family) treat this root as the identity of a multiplicative calculus tied to reciprocal quadratics; the case $t = 2$ is their base point.
In the broader Recognition framework the same identity $X + X^{-1} = 2$ is exactly where the T5 J-cost vanishes, so the lemma pins the neutral rung of any phi-ladder or eight-tick counting argument that routes through real traces. The dependency graph currently lists no downstream users, yet the evaluation is the natural base case for any normalization or induction on those identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.