SatisfiesDAlembert
plain-language theorem explainer
Predicate for the discrete d'Alembert law on integer-indexed sequences valued in the golden integers: h(m+n)+h(m−n)=h(m)·h(n). Cited by anyone running T5 cost-uniqueness on the φ-ladder rather than on ℝ. Pure Prop definition; no proof content.
Claim. A map $h:\mathbb{Z}\to\mathbb{Z}[\varphi]$ satisfies the discrete d'Alembert composition law when, for all $m,n\in\mathbb{Z}$, $$h(m+n)+h(m-n)=h(m)\cdot h(n).$$
background
The ambient module re-derives the T5 cost-uniqueness node on the forced discrete carrier of Recognition Science: the φ-ladder ${\varphi^n:n\in\mathbb{Z}}$, realized inside the golden ring $\mathbb{Z}[\varphi]$ (pairs $(a,b)$ for $a+b\varphi$ with $\varphi^2=\varphi+1$). On $\mathbb{R}$, the Recognition Composition Law folds, after the substitution $x=e^s$ and the shift $G=2F+2$, into the classical d'Alembert equation $G(s+t)+G(s-t)=G(s)G(t)$. Continuity and ODE uniqueness are then needed only to kill pathological solutions on an uncountable domain.
On the ladder those pathologies cannot arise. The natural carrier is the two-sided trace $t(n)=\varphi^n+\varphi^{-n}$ (exact $\mathbb{Z}[\varphi]$ avatar of $2\cosh(n\log\varphi)$). The present predicate is exactly the algebraic relation that $t$ obeys, and that any competing sequence must obey, before initial values pin it by induction.
A parallel continuous gate exists in the FourthGate development: there the structure is stated for $H:\mathbb{R}\to\mathbb{R}$ with normalization $H(0)=1$ and a factor of $2$ on the right-hand side. The discrete form here absorbs that scaling into the trace (no extra $2$) and leaves normalization out of the Prop itself.
proof idea
Definition only. The body is the single universal statement $\forall m,n:\mathbb{Z},; h(m+n)+h(m-n)=h(m)\cdot h(n)$ over the codomain GoldenInt. No tactics, no lemmas applied.
why it matters
This is the algebraic skeleton of the choice-free T5 argument on the φ-ladder. Existence (the ladder trace satisfies the law) is a pure ring identity via the exponential law for $\varphi^{\pm n}$. Uniqueness then follows by two-step strong induction from the initial data $h(0)=2$ and $h(1)=\sqrt{5}=2\varphi-1$, with evenness $h(-n)=h(n)$ derived from the law rather than assumed. The shifted sequence $G(n)=t(n)-2$ inherits the exact discrete RCL and is the unique normalized, calibrated solution, recovering $J(\varphi^n)$ without continuity or Classical.choice.
That closes the continuum gap flagged in the trichotomy read of the original real-variable T5 proof: the analytic cosh-ODE core is unnecessary once the domain is the T6 self-similar ladder. Downstream, the same shape feeds the continuous FourthGate classification (cosh as the smooth d'Alembert solution, exclusion of the quadratic log-lift) by supplying the discrete prototype of the $G$-side identity behind composition_law_equiv_coshAdd.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.