pow_eq_coords

The ambient setting is the cost/trace calculus for real units: numbers $u>1$ whose trace $u+u^{-1}$ is rational. Such a $u$ satisfies the monic quadratic $x^2-tx+1=0$, so the field $\mathbb{Q}(u)$ is at most quadratic. The complementary generator $d:=u-u^{-1}$ is the natural second basis vector; the pair ${1,d}$ spans the same $\mathbb{Q}$-vector space as ${1,u}$.

Elementary algebra gives the two identities used throughout: $u=t/2+d/2$ and $d^2=t^2-4$. Because $u>1$ one also has $t>2$, so $d^2>0$ and $d$ itself is nonzero. The module develops the consequence that a genuinely quadratic unit can never have a rational power: the second coordinate on ${1,d}$ refuses to vanish.

The present lemma is the coordinate expansion that makes that non-vanishing quantitative. Both coordinates are forced to be strictly positive rationals, not merely rational.

First record $u>0$, deduce $t>2$ from $(u-1)^2/u=u+u^{-1}-2>0$, and introduce $d=u-u^{-1}$. The two ring identities $u=t/2+d/2$ and $d^2=t^2-4$ are immediate.

Proceed by induction on $k$. The zero case is excluded by the hypothesis $k\ge 1$. For the successor step, split on whether $k=1$ or $k>1$. The base $k=1$ is exactly $u=t/2+(1/2),d$, so take $a=t/2$ and $b=1/2$ (both positive since $t>2$).

In the inductive step, write $u^n=a+b,d$ with $a,b\in\mathbb{Q}_{>0}$. Multiply by $u$ via $u^{n+1}=(a+bd)(t/2+d/2)$ and reduce $d^2$ by $t^2-4$. The resulting coordinates are $a'=a(t/2)+b(t^2-4)/2$ and $b'=a/2+b(t/2)$, both positive rationals by $t>2$ and positivity of $a,b$. The equality is discharged by a single linear_combination against the two base identities.

The unique downstream consumer is rat_of_trace_rat_of_pow_rat: if $u>1$ has rational trace and some positive power $u^q$ is itself rational, then $u$ is rational. That theorem simply invokes the coordinate expansion, notes that the second coordinate $b$ is a positive rational (hence nonzero as a real), and solves $u^q=A$ for the irrational part, forcing $d=0$ and therefore $u\in\mathbb{Q}$.

In the Recognition cost layer this is the algebraic reason the trace formulation is tractable. A unit that is genuinely quadratic over $\mathbb{Q}$ can never land on a rational after any positive power; the strictly positive second coordinate is exactly the obstruction. The lemma therefore underwrites every later argument that treats rational-trace units as either rational or free of rational powers, which is the dichotomy used when comparing cost values and ladder exponents.

It does not itself invoke the J-cost, the forcing chain, or the golden ratio; those enter only when the rationality dichotomy is applied to concrete RS units such as powers of $\varphi$.