ladder_ratio_real_brackets
plain-language theorem explainer
The classical golden ratio and its fifth and eighth powers sit in explicit rational intervals: 1.618033 < φ < 1.618034, 11.09 < φ⁵ < 11.10, and 46.978 < φ⁸ < 46.979. Anyone citing the continuum display of the forced ladder ratios uses this. The proof only transports already-decided integer brackets across the GoldenInt-to-ℝ evaluation map.
Claim. One has $1.618033 < \varphi < 1.618034$, together with $11.09 < \varphi^5 < 11.10$ and $46.978 < \varphi^8 < 46.979$, where $\varphi$ is the classical positive golden ratio.
background
The module GoldenIntReal is the sigma1 display bridge from the integer ring $\mathbb{Z}[\varphi]$ into $\mathbb{R}$. Derivation of T6 (φ forced as the unique positive golden root) lives entirely in GoldenInt at sigma0; this file evaluates $a + b\cdot\varphi \mapsto a + b\cdot\varphi_{\mathbb{R}}$ once, paying Classical.choice only at the continuum boundary.
The predicates RatLt and RatGt are the sigma0 rational lower/upper brackets on GoldenInt elements. The lemmas ratLt_toReal and ratGt_toReal say that, for positive denominator, those predicates are exactly the real inequalities $p/q < \mathrm{toReal},x$ and $\mathrm{toReal},x < p/q$. Separately, toReal_phi identifies the sigma0 unit with PhiForcing.φ, and toReal_phiPow sends the computable ladder phiPow n to the classical power $\varphi^n$.
Upstream, LadderRatioBounds already pins φ, φ⁵, and φ⁸ inside rational intervals by decide on integer arithmetic (e.g. phi5_lower: RatLt 1109 100 (phiPow 5)). This theorem only reads those brackets under evaluation.
proof idea
Six one-line transports. Apply ratLt_toReal (resp. ratGt_toReal) to the six sigma0 brackets phi_lower, phi_upper, phi5_lower, phi5_upper, phi8_lower, phi8_upper, each with a norm_num positivity check on the denominator. Rewrite the left-hand sides by toReal_phi on the φ pair and by toReal_phiPow on the φ⁵ and φ⁸ pairs, push integer casts to ℝ, and pack the six real inequalities into the nested conjunction.
why it matters
Closes the display half of the forced-ratio thread: the delta-forced rational brackets on φ, φ⁵, and φ⁸ become genuine real inequalities on the classical golden ratio. That is the continuum face of T6 (φ as self-similar fixed point) and of the ladder rungs used for RS-native constants (φ⁵ appears in ħ and G; φ⁸ is the octave rung tied to the eight-tick period).
Downstream, LadderRatioBounds packages the sigma0 side of the same brackets; this theorem is the bridge that lets continuum consumers cite the intervals without re-entering ℤ[φ]. No open scaffold remains: claim_status is proved, and the arithmetic was already discharged by decide at sigma0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.