golden_square_has_trace_three
plain-language theorem explainer
The square of the golden ratio, $u=(3+\sqrt{5})/2$, satisfies the multiplicative trace identity $u+u^{-1}=3$. Cost and PRC ledger arguments that rule out rational characters at trace three cite this as the concrete real witness. The proof is a short field-simplification closed by nonlinear arithmetic from $(\sqrt{5})^2=5$.
Claim. Let $u = \dfrac{3 + \sqrt{5}}{2}$. Then $u + u^{-1} = 3$.
background
In the Cost.TraceRationalExponent setting, the multiplicative trace of a positive real $u$ is the sum $u+u^{-1}$. When that sum is rational and $u>1$, the powers of $u$ live in a quadratic extension $\mathbb{Q}(\sqrt{d})$ with basis ${1,d}$ where $d=u-u^{-1}$. The module's arithmetic core records that both coordinates stay strictly positive rationals, so the irrational part cannot cancel.
The concrete $u$ here is $\varphi^2$, the square of the golden ratio $\varphi=(1+\sqrt{5})/2$. Recognition Science forces $\varphi$ as the self-similar fixed point (T6) and uses the J-cost $J(x)=(x+x^{-1})/2-1$, so a trace of three is the elementary real input behind any later claim that no rational character sits at that trace.
Sibling results in the same file (no rational square root of five; no rational character at trace three) turn this numerical identity into an obstruction against rational powers landing back in $\mathbb{Q}$.
proof idea
Three elementary facts are recorded: $(\sqrt{5})^2=5$ via Real.sq_sqrt, nonnegativity of $\sqrt{5}$, and nonzero-ness of $(3+\sqrt{5})/2$ by positivity. After field_simp clears the inverse, nlinarith finishes the equality from those three facts. No upstream Recognition lemmas are required; the argument is pure real arithmetic.
why it matters
This is the explicit real witness that the square of the golden ratio has trace three, so later obstruction theorems can name a concrete $u$ rather than an abstract quadratic unit. Downstream, cubeGeneratedNativeCost_two_not_canonical uses the rational-trace/power machinery of this module to show that the cube-generated native cost at two is not cross-equal to the on-ratio-orbit cost, i.e. is not canonical in the PRC structural ledger.
In the broader framework the identity sits under T5/T6: J-uniqueness and the forcing of $\varphi$. Because $J(u)=(u+u^{-1})/2-1$, trace three means $J(\varphi^2)=1/2$, a clean rung on the phi-ladder cost calculus that feeds native-cost canonicity arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.