realTraceRoot_add_inv
plain-language theorem explainer
For every real t ≥ 2, the principal root ρ(t) of X² − tX + 1 = 0 satisfies ρ(t) + 1/ρ(t) = t. Cost and character-factorization arguments cite this to convert between doubled-trace coordinates and multiplicative roots. The proof identifies the reciprocal with the conjugate branch (t − √(t²−4))/2 via a product identity, then cancels by ring.
Claim. Let $t \in \mathbb{R}$ with $t \ge 2$, and let $\rho(t) = \bigl(t + \sqrt{t^2-4}\bigr)/2$ be the principal ($\ge 1$) root of $X^2 - tX + 1 = 0$. Then $\rho(t) + \rho(t)^{-1} = t$.
background
In the real-trace cost module, the principal branch realTraceRoot t is defined as $(t + \sqrt{t^2-4})/2$ for $t \ge 2$. By construction it is the larger root of the monic quadratic $X^2 - tX + 1 = 0$, so its product with the conjugate branch is 1 and both roots are positive once $t \ge 2$.
The nonnegativity lemma $t^2-4 \ge 0$ legitimizes the square root, and positivity of the principal root (which follows from $\rho(t) \ge 1$) guarantees that the reciprocal is well-defined. These facts sit inside the same Cost layer that packages d'Alembert-type identities for real traces $T$ with $T(1)=2$, the doubled-trace normalization of the Recognition Composition Law side of the J-cost calculus.
Upstream, the definition and the two positivity/domain lemmas are the only local ingredients; the Clifford and finite-character imports appearing in the dependency graph are ambient module noise, not used in the argument.
proof idea
First apply the domain lemma to obtain $\sqrt{t^2-4}^2 = t^2-4$. Positivity of the principal root gives a nonzero denominator. The key algebraic step shows that the principal root times the conjugate branch $(t-\sqrt{t^2-4})/2$ equals 1: unfold the definition, clear denominators, and finish with nlinarith on the squared-radical identity. Dividing that product identity by the principal root identifies the reciprocal with the conjugate. Substitute, unfold the definition again, and close by ring.
why it matters
The identity is the bridge from additive trace coordinates back to multiplicative roots. Downstream, anchorRoot_add_inv specializes it to the rational trace of a ratio-orbit map under the Sans-anchor hypotheses, writing the anchor root plus its inverse as the displayed trace at 2. The sibling difference-square theorem mulDAlembert_diff_sq_trace also consumes it when reducing doubled-trace d'Alembert identities $(T(xy)+T(x/y)=T(x)T(y))$ with $T(1)=2$ to product formulas for $(T(xy)-T(x/y))^2$.
In the broader Recognition framework this is the real-analytic half of the J-cost story: $t = \rho + \rho^{-1}$ is exactly the coordinate in which $J$ becomes a pure shift of the Chebyshev/cosh generator forced at T5, and the d'Alembert form of the Recognition Composition Law is written in those coordinates. Closing the reciprocal identity keeps the principal-branch calculus free of case splits when factoring real characters and when lifting octave-period constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.