dAlembert_unique
plain-language theorem explainer
Any integer-indexed sequence in the golden integers that obeys d'Alembert's law and matches the ladder trace at 0 and 1 equals the trace at every integer. Downstream discrete RCL uniqueness cites it to pin the doubled J-cost on the φ-ladder. The argument is two-step strong induction on naturals, then derived evenness for negatives; no continuity or choice.
Claim. Let $h:\mathbb{Z}\to\mathbb{Z}[\varphi]$ satisfy $h(m+n)+h(m-n)=h(m)\,h(n)$ for all $m,n\in\mathbb{Z}$, with $h(0)=2$ and $h(1)=\sqrt{5}$. Then $h(n)=\varphi^n+\varphi^{-n}$ for every $n\in\mathbb{Z}$.
background
This module re-derives the T5 cost-uniqueness node on the discrete carrier forced by T6: the φ-ladder inside the golden integers $\mathbb{Z}[\varphi]$. On $\mathbb{R}$, uniqueness of the reciprocal-symmetric normalized continuous solution of the Recognition Composition Law needs a cosh ODE argument and classical choice. On ${\varphi^n:n\in\mathbb{Z}}$ the same algebraic skeleton is a two-step recurrence, so two initial values pin the solution by induction alone.
The d'Alembert predicate on sequences $h:\mathbb{Z}\to\mathbb{Z}[\varphi]$ is $h(m+n)+h(m-n)=h(m),h(n)$. It is the $G$-side shape of the continuum composition-law equivalence, discretized to the ladder. The ladder trace $\mathrm{tr}(n)=\varphi^n+\varphi^{-n}$ (the exact ring carrier of $2\cosh(n\log\varphi)$) satisfies that law algebraically, with $\mathrm{tr}(0)=2$ and $\mathrm{tr}(1)=\sqrt{5}=2\varphi-1$.
Negative powers stay inside the ring via $\varphi^{-1}=\varphi-1$; no field division is required.
proof idea
First prove agreement on $\mathbb{N}$ by strong induction. Base cases $k=0,1$ are the two given initial values against the known trace values. For $k+2$, rewrite the integer casts, invoke the inductive hypotheses at $k$ and $k+1$, then apply the one-step recurrence lemma (d'Alembert with the calibration $h(1)=\sqrt{5}$ forces $h(n+2)=h(1),h(n+1)-h(n)$) and the matching step identity for the trace.
For a general integer, split into nonnegatives and negative successors. Nonnegatives are the key lemma. Negatives use the derived symmetry $h(-n)=h(n)$ (obtained from d'Alembert plus $h(0)=2$, not assumed) together with the trace's evenness, reducing to the nonnegative case.
why it matters
This is the uniqueness half of the sigma0 T5 package on the delta spine. The continuum proof law_of_logic_forces_jcost needs continuity to kill pathological solutions on uncountable $\mathbb{R}$; here the recurrence leaves no room for them, so the axiom footprint drops to pure constructive algebra.
The sole direct consumer is discrete RCL uniqueness: any sequence obeying the discrete Recognition Composition Law with normalization $G(0)=0$ and calibration $G(1)=\sqrt{5}-2$ is the doubled J-cost $G(n)=\mathrm{tr}(n)-2=2J(\varphi^n)$. That argument shifts by 2 into the d'Alembert frame and applies this theorem.
Together they close the choice-free re-derivation of T5 (J-uniqueness) on the T6-forced carrier, feeding the discrete form of the RCL that the continuum theory writes as $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.