traceZ_step
plain-language theorem explainer
The ladder trace t(n)=φⁿ+φ⁻ⁿ on GoldenInt obeys the two-step recurrence t(n+2)=√5·t(n+1)−t(n) for every integer n. Anyone building the discrete T5 uniqueness argument cites this existence instance. The proof is a one-line specialization of the general d'Alembert step lemma to the trace sequence.
Claim. For every $n \in \mathbb{Z}$, the ladder trace $t(n) = \varphi^n + \varphi^{-n}$ (valued in $\mathbb{Z}[\varphi]$) satisfies $t(n+2) = \sqrt{5}\, t(n+1) - t(n)$, where $\sqrt{5}$ is the exact golden-integer $2\varphi-1$.
background
This module re-derives the T5 cost-uniqueness node on the forced discrete carrier: the φ-ladder {φⁿ : n ∈ ℤ} inside GoldenInt = ℤ[φ]. Continuum T5 proves that any reciprocal-symmetric, normalized, calibrated continuous F obeying the Recognition Composition Law equals J(x)=(x+x⁻¹)/2−1, but needs Classical.choice to kill pathological solutions of the cosh ODE. On the ladder those pathologies cannot exist.
The carrier of 2·cosh(n·log φ) is the exact sequence t(n)=φⁿ+φ⁻ⁿ. It satisfies d'Alembert's functional equation t(m+n)+t(m−n)=t(m)·t(n) purely algebraically. Specializing to the second argument equal to 1 yields the linear recurrence that replaces the ODE: a second-order recurrence is pinned by two initial values.
Upstream, the general step lemma states that any h:ℤ→GoldenInt with h(1)=√5 and SatisfiesDAlembert obeys h(n+2)=√5·h(n+1)−h(n). Here √5 is the ring element ⟨−1,2⟩=2φ−1, not a real square root.
proof idea
One-line wrapper: apply the general d'Alembert step lemma to the concrete sequence traceZ, feeding the already-proved facts that traceZ(1)=√5 and that traceZ satisfies d'Alembert. No further algebra is performed at this site.
why it matters
This is the existence half of the discrete replacement for ode_cosh_uniqueness_contdiff. Downstream, dAlembert_unique uses the recurrence (via two-step strong induction on ℕ, then derived evenness) to prove that any sequence obeying d'Alembert with the same two initial values h(0)=2, h(1)=√5 coincides with the trace on all of ℤ. That uniqueness theorem is the sigma0 T5 node: no continuity hypothesis, no Classical.choice.
In the forcing chain this closes the discrete path to T5 (J-uniqueness) on the T6 self-similar carrier. The same recurrence later yields that G(n)=t(n)−2 is the unique discrete RCL solution with the normalization and calibration of 2·J(φⁿ), completing the cost-uniqueness spine without continuum analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.