toReal_traceZ
plain-language theorem explainer
The integer trace sequence t(n)=φⁿ+φ⁻ⁿ in ℤ[φ] evaluates under the real display map to the classical two-sided power sum φ_ℝⁿ+φ_ℝ⁻ⁿ. Anyone bridging the sigma0 discrete cost ladder to real J-cost or cosh identities cites this. The proof is a three-line rewrite: unfold the sum, apply additivity of the display, then the unit-power evaluation twice.
Claim. For every integer $n$, the real evaluation of the golden-integer trace $t(n)=\varphi^n+\varphi^{-n}$ equals $\varphi_{\mathbb{R}}^n+\varphi_{\mathbb{R}}^{-n}$, where $\varphi_{\mathbb{R}}$ is the classical positive golden ratio.
background
This module is the sigma1 display bridge from the discrete ring ℤ[φ] to ℝ. The evaluation map sends a+b·φ to a+b·φ_ℝ; it is a ring embedding, and the sigma0 golden unit maps to the classical PhiForcing root. Only this continuum step costs Classical.choice; the forcing derivation itself stays delta-closed.
Upstream, the trace sequence is defined inside ℤ[φ] as the sum of unit-group powers φⁿ+φ⁻ⁿ (exact ring elements for negative exponents). A prior lemma already shows that each such power evaluates to the corresponding real integer power of φ_ℝ. Additivity of the display is elementary from the coordinate definition.
The local goal is to push the entire two-sided sum across the boundary so that classical identities (cosh, J-cost) become available without re-deriving the ladder in ℝ.
proof idea
Unfold the definition of the trace as the sum of the two unit powers. Rewrite the left-hand side by additivity of the real evaluation, then replace each summand by the already-proved evaluation of unit powers. The goal is then definitionally the classical two-sided power sum. No induction or analysis is needed at this step; the work sits in the power-evaluation lemma.
why it matters
This is the hinge between the discrete sigma0 trace and the classical continuum presentation of the cost. Downstream, the cosh display rewrites the same evaluation as 2·cosh(n·log φ), identifying the d'Alembert equation proved at sigma0 with the addition law of cosh. The J-cost display uses it to show that the doubled discrete cost evaluates to 2·J(φⁿ) for the canonical cost J(x)=(x+x⁻¹)/2−1, which is exactly the T5 unique solution of the Recognition Composition Law.
Together these close the display of the forcing chain's cost uniqueness into real analysis: the discrete RCL becomes the functional equation that forces J, and the ladder becomes the hyperbolic one-parameter group. Without this identity the continuum tax would have to be paid again inside each cost theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.