SatisfiesDiscreteRCL
plain-language theorem explainer
Predicate that a map G from integers into the golden integers obeys the discrete Recognition Composition Law: G(m+n)+G(m−n)=G(m)G(n)+2G(m)+2G(n) for all m,n. This is the continuum RCL specialized to pure φ-powers with doubled normalization so values stay in ℤ[φ]. Existence and uniqueness proofs for the discrete T5 cost cite it as the composition hypothesis. Pure definitional Prop; no proof content.
Claim. A map $G:\mathbb{Z}\to\mathbb{Z}[\varphi]$ satisfies the discrete Recognition Composition Law when $G(m+n)+G(m-n)=G(m)\,G(n)+2\,G(m)+2\,G(n)$ for all integers $m,n$. This is the composition law for the doubled cost $G=2F$ on pure powers $x=\varphi^m$, $y=\varphi^n$ (so $xy=\varphi^{m+n}$ and $x/y=\varphi^{m-n}$).
background
The Recognition Composition Law (RCL) is the functional equation $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ that forces the J-cost $J(x)=(x+x^{-1})/2-1$ in the continuum T5 argument. On the φ-ladder forced by T6 self-similarity one substitutes $x=\varphi^m$, $y=\varphi^n$ and works with the doubled normalization $G=2F$ so every value lands in the golden ring $\mathbb{Z}[\varphi]$: pairs $(a,b)$ for $a+b\varphi$ with multiplication folded through $\varphi^2=\varphi+1$.
This module re-derives T5 choice-free on that discrete carrier. Continuum cosh-ODE uniqueness is replaced by a two-step recurrence pinned by two initial values. The doubled J-cost is $J_{\mathrm{double}}(n)=\varphi^n+\varphi^{-n}-2=2J(\varphi^n)$, carried by the algebraic trace $\mathrm{traceZ},n=\varphi^n+\varphi^{-n}$, which itself obeys d'Alembert's law $t(m+n)+t(m-n)=t(m)t(n)$.
proof idea
Definitional predicate only. The body is the universal quantification, over all integers $m,n$, of the discrete RCL identity with addition and multiplication taken in GoldenInt. No tactics, no lemmas, no proof term beyond the Prop itself. Downstream theorems inhabit this interface: existence unfolds the doubled cost and rearranges the trace d'Alembert identity; uniqueness shifts by 2 into the d'Alembert frame and applies trace uniqueness.
why it matters
This is the discrete stand-in for the continuum SatisfiesCompositionLaw shape and the composition hypothesis of the sigma0 T5 node. Downstream, Jdouble_rcl proves the doubled J-cost satisfies it by linear rearrangement of the d'Alembert identity for traceZ; discreteRCL_unique shows any G with normalization $G(0)=0$, calibration $G(1)=\sqrt{5}-2$, and this law equals the doubled J-cost; t5_delta_forced packages existence, uniqueness, derived reciprocity, and the discrete RCL into the choice-free T5 statement on the φ-ladder. It closes the continuum-to-discrete reduction of forcing-chain T5 (J-uniqueness) without Classical.choice, matching the module's trichotomy read that pathology lives only on uncountable $\mathbb{R}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.