toReal_phiZpow
plain-language theorem explainer
The integer power ladder of φ inside ℤ[φ] evaluates under the real embedding to ordinary real powers of the classical golden ratio. Anyone bridging sigma0 ladder identities to continuum statements cites this. The proof is integer induction on n, using the exponential law and the base cases toReal(φ)=φ and toReal(φ⁻¹)=φ⁻¹.
Claim. For every integer $n$, the real evaluation of the unit-group power $\varphi^n \in \mathbb{Z}[\varphi]$ equals the classical real power: $\mathrm{toReal}(\varphi^n) = \varphi_{\mathbb{R}}^n$, where $\varphi_{\mathbb{R}}$ is the positive golden root forced by PhiForcing.
background
GoldenIntReal is the display bridge from the discrete ring $\mathbb{Z}[\varphi]$ to $\mathbb{R}$. The derivation of T6 (φ forced as the unique positive golden root) lives entirely inside $\mathbb{Z}[\varphi]$ with delta-forced axiom closure; this module pays the continuum tax once by evaluating $a+b\varphi\mapsto a+b\varphi_{\mathbb{R}}$.
The map toReal is a ring embedding. The unit-group ladder phiZpow n is $\varphi^n$ for $n:\mathbb{Z}$, so negative exponents are exact ring elements (via phiInv = $\varphi-1 = \langle -1,1\rangle$), not divisions. Upstream, phiZpow_add gives the exponential law $\varphi^{m+n}=\varphi^m\cdot\varphi^n$, and the base identities fix phiZpow 0 = 1, phiZpow 1 = $\varphi$, phiZpow (-1) = phiInv.
The classical target is PhiForcing.φ, the unique positive root of $x^2=x+1$. The claim is that the discrete ladder and the real power ladder coincide under evaluation.
proof idea
Integer induction on $n$ via Int.induction_on, after recording $\varphi_{\mathbb{R}}\neq 0$ from positivity.
Zero case: rewrite with phiZpow_zero, toReal_one, and zpow_zero.
Successor: the step identity phiZpow(k+1)=phiZpow k · φ comes from phiZpow_add and phiZpow_one. Apply toReal_mul, the inductive hypothesis, toReal_phi, then zpow_add_one.
Predecessor: rewrite $-(k)-1=-(k)+(-1)$, then phiZpow_add and phiZpow_neg_one give multiplication by phiInv. Apply toReal_mul, IH, toReal_phiInv, and zpow_sub_one.
why it matters
This is the integer-power half of the sigma0-to-classical display. Downstream, toReal_phiPow reduces the computable $\mathbb{N}$-ladder to this theorem plus zpow_natCast, and toReal_traceZ uses it twice to identify the discrete trace sequence with $\varphi^n+\varphi^{-n}$ (the classical two-sided power sum, equivalently $2\cosh(n\log\varphi)$).
In the Recognition forcing chain, T6 forces φ as the self-similar fixed point inside $\mathbb{Z}[\varphi]$. Continuum statements about ladder ratios, mass rungs, and cost uniqueness need the evaluation to match ordinary real powers; without this bridge those inequalities would remain private to the discrete ring. The module's t6_bridge and ladder-ratio display results sit on top of this identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.