toReal_phiPow
plain-language theorem explainer
The natural-number φ-ladder in ℤ[φ], once evaluated into ℝ, equals ordinary real powers of the classical golden ratio. Anyone bridging sigma0 ladder certificates to continuum inequalities cites this. The proof is a three-step rewrite: identify the ℕ-ladder with the ℤ-ladder, apply the integer-power evaluation lemma, then coerce the exponent.
Claim. For every natural number $n$, the real evaluation of the computable $\varphi$-ladder element $\varphi^n \in \mathbb{Z}[\varphi]$ equals the classical real power $\varphi_{\mathbb{R}}^n$, where evaluation is $a + b\varphi \mapsto a + b\varphi_{\mathbb{R}}$.
background
GoldenIntReal is the sigma1 display bridge from the choice-free ring $\mathbb{Z}[\varphi]$ to $\mathbb{R}$. The derivation of T6 (φ forced as the unique positive golden root) lives entirely in GoldenInt at sigma0; this module pays the continuum tax once by evaluating $\langle a,b\rangle \mapsto a + b\cdot\varphi_{\mathbb{R}}$.
The φ-ladder is the fundamental scale structure of Recognition Science: powers of φ form the discrete mass and coupling rungs. In the algebra layer, phiPow builds $\varphi^n$ inside $\mathbb{Z}[\varphi]$ by the Fibonacci recurrence. A companion integer ladder phiZpow covers $\mathbb{Z}$-exponents. The evaluation map toReal is already known to send the integer ladder to real zpowers (toReal_phiZpow: "the unit-group power ladder evaluates to real integer powers of φ").
This lemma specializes that fact to natural exponents, matching the ℕ-indexed rungs used by ladder-ratio brackets and mass-window certificates.
proof idea
Three rewrites, no induction. First phiPow_eq_phiZpow identifies the natural ladder with the integer ladder at $n:\mathbb{N}$. Then toReal_phiZpow converts that integer ladder element into $\varphi_{\mathbb{R}}^n$ as a zpower. Finally zpow_natCast rewrites the zpower with natural exponent as an ordinary real power. The heavy lifting (induction on $\mathbb{Z}$, multiplicativity of toReal, $\varphi\neq 0$) already sits in toReal_phiZpow.
why it matters
Without this bridge, sigma0 rational brackets on ladder rungs stay trapped in $\mathbb{Z}[\varphi]$. Downstream, ladder_ratio_real_brackets uses it so that the forced-ratio thread (φ, φ⁵, φ⁸ pinned by decide at sigma0) reads as genuine real inequalities on classical φ. Mass-ratio binding then rewrites with it repeatedly: muE_window_between_rungs gets $\varphi^{11}<R<\varphi^{12}$, muE_sq_between gets $\varphi^{21}<R^2<\varphi^{23}$, and the deviation certificates muE_pow63_gt / muE_pow88_lt compare high powers of R against φ-ladder rungs.
In the forcing chain this supports the T6 display (φ as self-similar fixed point) and the φ-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). It is pure transport: arithmetic was decided choice-free; only the continuum reading costs Classical.choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.