traceZ_dAlembert
plain-language theorem explainer
The integer-indexed trace t(n)=φⁿ+φ⁻ⁿ on the golden integers satisfies d'Alembert's law t(m+n)+t(m−n)=t(m)·t(n). Anyone citing discrete T5 cost uniqueness on the φ-ladder needs this existence half. The proof is pure algebra: expand both sides through the exponential law for φ^ℤ and finish with ring.
Claim. Let $t:\mathbb{Z}\to\mathbb{Z}[\varphi]$ be $t(n)=\varphi^n+\varphi^{-n}$. Then for all $m,n\in\mathbb{Z}$, $t(m+n)+t(m-n)=t(m)\,t(n)$.
background
This module re-derives the T5 cost-uniqueness node on the discrete carrier forced by T6: the φ-ladder {φⁿ : n∈ℤ} inside GoldenInt=ℤ[φ]. The continuum proof of T5 folds the Recognition Composition Law into d'Alembert for G=2F+2 and then uses a cosh ODE argument; on the ladder that analytic core is unnecessary, because a two-step recurrence plus two initial values pins every solution by induction, with no continuity and no Classical.choice.
Here phiZpow n is φⁿ realized through the unit group GoldenIntˣ, so negative exponents are exact ring elements (φ⁻¹=φ−1). The trace is traceZ n = φⁿ + φ⁻ⁿ, the exact ℤ[φ] carrier of 2 cosh(n log φ). SatisfiesDAlembert is the discrete G-side law: h(m+n)+h(m−n)=h(m)·h(n), the ladder form of the composition-law equivalence used upstream in Cost.FunctionalEquation.
The exponential law phiZpow_add (φ^(m+n)=φ^m·φ^n) is the only nontrivial input; everything else is ring arithmetic on GoldenInt.
proof idea
Tactic proof, purely algebraic. Introduce m,n and unfold traceZ on both sides. Four applications of phiZpow_add rewrite the four powers:
- φ^(m+n)=φ^m·φ^n
- φ^(-(m+n))=φ^(-m)·φ^(-n) (after -(m+n)=-m+-n)
- φ^(m-n)=φ^m·φ^(-n) (after m-n=m+-n)
- φ^(-(m-n))=φ^(-m)·φ^n (after -(m-n)=-m+n)
Substitute those equalities; the resulting polynomial identity in the four factors φ^(±m), φ^(±n) is discharged by ring.
why it matters
Existence half of the discrete d'Alembert node on the φ-ladder: without it there is no discrete T5. Downstream, Jdouble_rcl obtains the discrete RCL for Jdouble n = traceZ n − 2 by linear rearrangement of this identity ("Existence: the doubled J-cost satisfies the discrete RCL"). Also, traceZ_step instantiates the two-step recurrence t(n+2)=√5·t(n+1)−t(n) via dAlembert_step, which uniqueness then runs by strong induction.
In the framework this is the sigma0 (choice-free) re-derivation of T5 J-uniqueness on the T6 carrier: J(x)=(x+x⁻¹)/2−1 is forced as the unique normalized, calibrated solution of RCL once the continuum pathologies are excluded by restricting to {φⁿ}. Reciprocal symmetry is not assumed; the next lemma derives it by setting m=0 in d'Alembert and cancelling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.