Jdouble_rcl
plain-language theorem explainer
The doubled J-cost on the φ-ladder satisfies the discrete Recognition Composition Law over ℤ[φ]. Anyone citing the choice-free (sigma0) re-derivation of T5 cost uniqueness needs this existence half. The proof is a linear rearrangement of the algebraic d'Alembert identity for the trace sequence, closed by ring.
Claim. Let $G(n)=\varphi^n+\varphi^{-n}-2$ for $n\in\mathbb{Z}$. Then for all integers $m,n$, $$G(m+n)+G(m-n)=G(m)G(n)+2G(m)+2G(n).$$ Equivalently, the doubled ladder cost $G=2J\circ\varphi^{(\cdot)}$ obeys the discrete RCL in the ring $\mathbb{Z}[\varphi]$.
background
This module re-derives the T5 cost-uniqueness node on the discrete carrier forced by T6: the φ-ladder ${\varphi^n:n\in\mathbb{Z}}$ inside the golden integers $\mathrm{GoldenInt}=\mathbb{Z}[\varphi]$. The continuum proof of T5 needs continuity and Classical.choice to kill pathological solutions of the RCL; on the ladder the same law is a two-step recurrence, so two initial values pin everything by induction.
The trace sequence is $\mathrm{traceZ}(n)=\varphi^n+\varphi^{-n}$, the exact ring carrier of $2\cosh(n\log\varphi)$. It satisfies d'Alembert: $t(m+n)+t(m-n)=t(m)t(n)$. The doubled J-cost is the shift $G(n)=\mathrm{traceZ}(n)-2=2J(\varphi^n)$, with $J(x)=(x+x^{-1})/2-1$. The discrete RCL is the exact shape of the continuous composition law with $x=\varphi^m$, $y=\varphi^n$, written in the doubled normalization so all values stay in the ring: $G(m+n)+G(m-n)=G(m)G(n)+2G(m)+2G(n)$.
proof idea
Tactic proof, purely algebraic. Fix integers $m,n$ and unfold $G=\mathrm{traceZ}-2$. Invoke the upstream existence lemma that $\mathrm{traceZ}$ obeys d'Alembert. Expand the target right-hand side by ring: $(t_m-2)(t_n-2)+2(t_m-2)+2(t_n-2)=t_m t_n-4$. Rewrite via d'Alembert so the left-hand side becomes $t_{m+n}+t_{m-n}-4$, which is exactly $G(m+n)+G(m-n)$. A final ring closes the equality. No induction and no analysis.
why it matters
This is the existence leg of discrete T5. The parent theorem t5_delta_forced packages it with normalization $G(0)=0$, calibration $G(1)=\sqrt{5}-2$, derived reciprocal symmetry, and uniqueness among all sequences satisfying the discrete RCL with those two pins. That parent is the sigma0 (choice-free) counterpart of the continuum T5 node law_of_logic_forces_jcost in the forcing chain: same J-cost, now forced on the T6 ladder without continuity or Classical.choice.
In the framework landmarks this closes the discrete half of T5 (J-uniqueness) once T6 has fixed the carrier. The continuous RCL rearranges to d'Alembert for $2F+2$; here the same rearrangement is exact in $\mathbb{Z}[\varphi]$. Downstream uniqueness then follows by two-step strong induction on the recurrence, not by ODE arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.