discreteRCL_unique
plain-language theorem explainer
Any integer-indexed sequence in ℤ[φ] that obeys the discrete Recognition Composition Law, with J-cost normalization G(0)=0 and calibration G(1)=√5−2, equals the doubled J-cost on the φ-ladder. The T5 delta-forced packaging theorem cites this uniqueness half. The proof shifts by 2 into the d'Alembert frame and applies algebraic trace uniqueness.
Claim. Let $G:\mathbb{Z}\to\mathbb{Z}[\varphi]$ satisfy $G(0)=0$, $G(1)=\sqrt{5}-2$, and the discrete RCL $$G(m+n)+G(m-n)=G(m)G(n)+2G(m)+2G(n)$$ for all $m,n\in\mathbb{Z}$. Then for every $n$, $G(n)=\varphi^n+\varphi^{-n}-2$ (equivalently $G(n)=2J(\varphi^n)$ with $J(x)=(x+x^{-1})/2-1$).
background
This module re-derives the T5 cost-uniqueness node on the discrete carrier forced by T6: the φ-ladder inside GoldenInt = ℤ[φ]. The continuum T5 result (law_of_logic_forces_jcost) needs continuity and Classical.choice to kill pathological solutions on ℝ. On ℤ those pathologies cannot arise; a two-step recurrence plus two initial values pins the sequence by induction.
The discrete RCL is the exact shape of the continuous Recognition Composition Law with $x=\varphi^m$, $y=\varphi^n$, written in the doubled normalization $G=2F$ so everything stays in the ring: $G(m+n)+G(m-n)=G(m)G(n)+2G(m)+2G(n)$.
The target sequence is Jdouble n = traceZ n − 2, where traceZ n = φⁿ + φ⁻ⁿ is the exact ℤ[φ] carrier of $2\cosh(n\log\varphi)$. Normalization is $G(0)=0$; calibration is $G(1)=\sqrt{5}-2=2J(\varphi)$. Reciprocity is not assumed: it is derived from the law.
proof idea
Define the shifted sequence $H(k)=G(k)+2$. Normalization and calibration become $H(0)=2$ and $H(1)=\sqrt{5}$. Expanding the discrete RCL and rearranging shows $H$ satisfies d'Alembert's functional equation $H(m+n)+H(m-n)=H(m)H(n)$.
Invoke the upstream uniqueness theorem for d'Alembert sequences on ℤ (two-step strong induction from the two initial values): $H=\mathrm{traceZ}$. Unfolding Jdouble n = traceZ n − 2 and cancelling the shift yields $G=\mathrm{Jdouble}$. The argument is pure ring algebra; no continuity or choice.
why it matters
This is the uniqueness half of the sigma0 T5 node on the forced discrete carrier. Downstream, t5_delta_forced packages it with existence, normalization, calibration, and derived reciprocity into the full statement: on the φ-ladder, the doubled J-cost is the unique sequence obeying discrete RCL plus the two calibrations.
In the forcing chain this discharges T5 (J-uniqueness) without the continuum residue quarantined in Cost.FunctionalEquation. The algebraic skeleton of RCL → d'Alembert is retained; the analytic cosh-ODE step is dropped because the ledger domain is ℤ, not ℝ. Audit closure is {propext, Quot.sound} only. Together with T6 (φ as self-similar fixed point) this locks the cost functional that later feeds mass ladders, the eight-tick octave, and the α band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.