realTraceRoot_mul
plain-language theorem explainer
The principal root of X² − tX + 1 = 0 multiplies under the hyperbolic addition formula for the trace. For a, b ≥ 2, the combined trace (ab + √(a²−4)√(b²−4))/2 has principal root equal to the product of the two individual principal roots. Cost-layer work on d'Alembert/trace identities cites this. Proof is direct algebra: discriminant identity, then field_simp and ring.
Claim. If $a,b\geq 2$ and $u=\frac{ab+\sqrt{a^2-4}\sqrt{b^2-4}}{2}$, then the principal ($\geq 1$) root of $X^2-uX+1=0$ equals the product of the principal roots of $X^2-aX+1=0$ and $X^2-bX+1=0$.
background
For a real parameter $t\geq 2$, the principal real trace root is the larger root of the monic reciprocal quadratic $X^2-tX+1=0$, namely $(t+\sqrt{t^2-4})/2$. It is always at least $1$ and satisfies $\rho+\rho^{-1}=t$. The elementary fact $t^2-4\geq 0$ for $t\geq 2$ underwrites every square-root step in the module.
This lives in Cost.RealTraceRoot, which builds real-analytic bookkeeping for traces that appear in d'Alembert-type composition laws. The same root is the larger eigenvalue of an SL(2)-type matrix of trace $t$, or the exponential scale attached to a cosh-parameter.
Upstream, the definition of the principal root and the nonnegativity lemma for the discriminant are the only local ingredients the argument needs.
proof idea
Set $s_a=\sqrt{a^2-4}$ and $s_b=\sqrt{b^2-4}$, using nonnegativity of the discriminants. Write $u=(ab+s_a s_b)/2$. Expand $4(u^2-4)$ by nlinarith against $s_a^2=a^2-4$ and $s_b^2=b^2-4$ to get $u^2-4=((a s_b+b s_a)/2)^2$. Take the nonnegative square root. Unfold the principal-root definition on both sides; both equal $(ab+a s_b+b s_a+s_a s_b)/4$ after field_simp and ring.
why it matters
This multiplication law moves identities between the multiplicative group variable and the trace coordinate. Downstream, the difference-square theorem in doubled-trace units (mulDAlembert_diff_sq_trace) converts a multiplicative composition law $T(xy)+T(x/y)=T(x)T(y)$ with $T(1)=2$ into $(T(xy)-T(x/y))^2=(T(x)^2-4)(T(y)^2-4)$, and the present root product is the algebraic engine behind that conversion.
In Recognition Science the cost is tied to $J(x)=(x+x^{-1})/2-1$ (T5 J-uniqueness), and the Recognition Composition Law is the d'Alembert form of that cost. Principal-branch multiplication is local infrastructure rather than a forcing-chain step, but the cost-layer trace calculus does not close without it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.