traceZ_zero
plain-language theorem explainer
The integer-indexed trace on the golden integers evaluates to 2 at the origin: φ⁰ + φ⁰ = 2. Anyone citing the discrete d'Alembert uniqueness or the normalized double-J sequence on the φ-ladder needs this base value. The proof unfolds the trace definition, collapses −0, applies φ⁰ = 1, and finishes by decidable arithmetic in GoldenInt.
Claim. Let $t:\mathbb{Z}\to\mathbb{Z}[\varphi]$ be the trace $t(n)=\varphi^n+\varphi^{-n}$. Then $t(0)=2$.
background
This module re-derives the T5 cost-uniqueness node on the discrete φ-ladder carrier forced by T6, working entirely inside GoldenInt = ℤ[φ] so that negative powers are ring elements (φ⁻¹ = φ − 1) rather than field inverses. The continuum proof of T5 reduces the Recognition Composition Law to d'Alembert's functional equation for G = 2F + 2 and then invokes analytic uniqueness of cosh; on {φⁿ : n ∈ ℤ} that analytic step is replaced by a two-step recurrence.
The trace sequence is defined by t(n) = φⁿ + φ⁻ⁿ via the unit-group powers phiZpow. It is the exact ℤ[φ] carrier of 2·cosh(n·log φ). The companion fact phiZpow 0 = 1 records that the zero power of the golden unit is the multiplicative identity. The value t(0) = 2 is the first initial condition that pins every d'Alembert solution on ℤ.
proof idea
Term-mode proof in three steps. Unfold traceZ to φ⁰ + φ⁻⁰. Rewrite with neg_zero (so −0 = 0) and phiZpow_zero (φ⁰ = 1), obtaining 1 + 1. Close by decide on the concrete GoldenInt equality 1 + 1 = 2.
why it matters
Supplies the normalization seed for the whole discrete T5 package. Downstream, dAlembert_unique takes h 0 = 2 together with h 1 = √5 and the d'Alembert law, then proves by two-step strong induction that any such h equals the trace; that uniqueness is the sigma0 replacement for the continuum cosh-ODE argument. Immediately after, Jdouble_zero rewrites Jdouble 0 = traceZ 0 − 2 through this lemma and obtains the RCL normalization G(0) = 0, i.e. 2·J(φ⁰) = 0.
In the forcing chain this is the discrete base case of T5 (J-uniqueness): once the trace is pinned, the double-J sequence is the unique normalized, calibrated solution of the exact discrete Recognition Composition Law on the φ-ladder, with no continuity hypothesis and no Classical.choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.