larger_trace_of_diff_sq
plain-language theorem explainer
Given sum u+v=ab and squared difference (u−v)²=(a²−4)(b²−4) with v≤u and a,b≥2, the larger value u equals the cosh-addition form (ab+√(a²−4)√(b²−4))/2. Used when recovering the larger doubled-trace from sum and difference data in the multiplicative d'Alembert algebra. Proof takes square roots (using nonnegativity of a²−4), multiplies the radicals, then solves the linear system by linarith.
Claim. If $a,b\ge 2$ and $u,v\in\mathbb{R}$ satisfy $u+v=ab$, $(u-v)^2=(a^2-4)(b^2-4)$, and $v\le u$, then $u=\bigl(ab+\sqrt{a^2-4}\,\sqrt{b^2-4}\bigr)/2$.
background
The module develops pure algebra for doubled-trace units: maps $T$ with $T(1)=2$ obeying the multiplicative d'Alembert law $T(xy)+T(x/y)=T(x)T(y)$. Writing $g=T/2$ recovers the classical form $g(xy)+g(x/y)=2g(x)g(y)$ with $g(1)=1$. These traces sit above the RS cost $J(x)=\cosh(\log x)-1$ via $T(x)=x+x^{-1}=2(J(x)+1)$ when $x>0$.
For $t\ge 2$ one has $t^2-4\ge 0$ (lemma realTraceRoot_sq_sub_four_nonneg), so $\sqrt{t^2-4}$ is well-defined and plays the role of a hyperbolic sine factor. The pair of identities $u+v=ab$ and $(u-v)^2=(a^2-4)(b^2-4)$ is exactly the sum/difference data for the two values $T(xy)$ and $T(x/y)$ when $a=T(x)$, $b=T(y)$.
The local goal is to name the larger root explicitly as the cosh-addition combination, matching the classical identity $\cosh(X+Y)=\cosh X\cosh Y+\sinh X\sinh Y$ after the change of variables $T=2\cosh$.
proof idea
From $a\ge 2$, invoke realTraceRoot_sq_sub_four_nonneg to get $a^2-4\ge 0$. Apply Real.sqrt_mul to factor $\sqrt{(a^2-4)(b^2-4)}=\sqrt{a^2-4},\sqrt{b^2-4}$.
Take Real.sqrt of both sides of the squared-difference hypothesis. Because $v\le u$, one has $u-v\ge 0$, so Real.sqrt_sq cancels the outer square and yields $u-v=\sqrt{a^2-4},\sqrt{b^2-4}$.
With sum $u+v=ab$ and difference $u-v$ in hand, a single linarith solves for $u$ as the stated average.
why it matters
This lemma is the algebraic recovery step for the larger doubled-trace in the multiplicative d'Alembert calculus. Downstream, mulDAlembert_diff_sq_trace uses the same sum/difference geometry (with $T(1)=2$) to prove $(T(xy)-T(x/y))^2=(T(x)^2-4)(T(y)^2-4)$ under the product law; the present identity is the converse direction that names the larger root.
In the Recognition framework the doubled-trace $T=x+x^{-1}$ is the natural lift of the unique cost $J$ forced at T5 ($J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$). The cosh-addition form is exactly how the Recognition Composition Law organises products on the positive reals. Closing the sum/difference algebra here keeps the pure-cost layer free of analytic baggage before it is wired into the phi-ladder and eight-tick structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.