traceZ
plain-language theorem explainer
The integer-indexed trace t(n)=φⁿ+φ⁻ⁿ is defined in the golden ring ℤ[φ] as the exact algebraic carrier of 2·cosh(n·log φ). Anyone proving cost uniqueness on the forced φ-ladder cites it as the canonical d'Alembert sequence. The body is a one-line sum of positive and negative ladder powers through the unit group.
Claim. For each integer $n$, the trace is the golden-ring element $t(n):=\varphi^n+\varphi^{-n}\in\mathbb{Z}[\varphi]$, where powers of $\varphi$ (including negative exponents) are taken through the unit group so that every value is an exact ring element.
background
CostUniqueness re-derives the T5 J-cost uniqueness node on the discrete φ-ladder rather than on ℝ. The continuum proof folds RCL into d'Alembert's functional equation and excludes pathologies by a cosh ODE argument that needs continuity and Classical.choice. On the ladder {φⁿ : n∈ℤ} forced by T6, the same law is a two-step recurrence pinned by two initial values, so no continuity axis is required.
The carrier is GoldenInt = ℤ[φ]: pairs (a,b) for a+b·φ with multiplication folded through φ²=φ+1. Ladder powers are phiZpow n = φⁿ, obtained by casting the unit-group power (phiUnit^n) back to the ring; negative exponents are exact because φ⁻¹=φ−1, with no division.
The trace is the natural even combination of those powers. It is the exact ℤ[φ] stand-in for 2·cosh(n·log φ), and therefore the discrete skeleton of the continuum cost.
proof idea
One-line definition: sum the ladder power at n with the ladder power at −n. Both sides are already GoldenInt via the unit-group embedding, so the sum is well-typed with no further proof obligations.
why it matters
This is step 2 of the module's sigma0 program: the exact carrier on which d'Alembert and discrete RCL are proved by pure algebra. Downstream, traceZ_dAlembert expands both sides of the functional equation through the exponential law and rings; traceZ_neg and the step lemmas feed the two-step induction in dAlembert_unique (any sequence with the same initial values equals the trace). Shifting by 2 yields Jdouble n = t(n)−2 = 2·J(φⁿ), whose discrete RCL existence and uniqueness (Jdouble_rcl, discreteRCL_unique) close T5 on the forced ladder without choice. Framework landmark: T5 J-uniqueness, now choice-free on the T6 carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.