phi5_lower
plain-language theorem explainer
The fifth φ-ladder rung sits strictly above 11.09: 1109/100 < φ⁵ in the golden integers (φ⁵ ≈ 11.0902). Anyone certifying RS mass ratios, the Z_cf ≈ φ⁵ band, or the Hubble-tension pipeline cites this bound. The proof is a single kernel `decide` on the decidable positivity predicate for the witness 100·φ⁵ − 1109.
Claim. The rational $1109/100$ lies strictly below $\varphi^5$ as an element of $\mathbb{Z}[\varphi]$, i.e. $11.09 < \varphi^5$ (with $\varphi^5 \approx 11.0902$).
background
The module LadderRatioBounds certifies forced φ-ladder ratios at sigma0 with rational brackets that both the kernel (decide) and runtime (#eval) close. In RS the mass law places spectrum rungs on the φ-ladder: two states separated by integer gap k stand in the exact dimensionless ratio φ^k. φ itself is the T6 fixed point; every ladder gap is an integer power of it.
Here phiPow n is φ^n built by structural recursion in ℤ[φ] (so phiPow 5 = ⟨3,5⟩ = 3+5φ), reducing under both kernel and compiler. The predicate RatLt p q x means the rational p/q lies strictly below x; it is the decidable integer claim IsPos(q·x − p). Because positivity on ℤ[φ] reduces to a sign question about s+t√5 decided by comparing s² with 5t² (√5-irrationality, no Real.sqrt, no Float, no native_decide), every concrete bracket lives in {propext, Quot.sound}.
The real-side reading of these brackets is deferred to GoldenIntReal (sigma1 CHOICE); the arithmetic itself is forced at sigma0.
proof idea
One-line tactic proof: by decide. The goal RatLt 1109 100 (phiPow 5) unfolds to positivity of the witness 100 · phiPow 5 − 1109 in ℤ[φ]. After reducing phiPow 5 by the Fibonacci recurrence to ⟨3,5⟩, the kernel compares integer squares against 5t² and closes the strict inequality without classical choice or floating-point evaluation.
why it matters
This is the lower half of the φ⁵ bracket in the forced-ratio thread. It feeds ladder_ratio_brackets, which bundles certified intervals for φ, φ⁵, and φ⁸ entirely by choice-free integer arithmetic, and the real bridge ladder_ratio_real_brackets (1109/100 < φ⁵ < 1110/100 over ℝ).
Downstream, the cosmology certificate HubbleTensionCert / hubbleTensionCert records phi5_lower among its fields, tying the ladder bound into the Hubble-tension pipeline from z-aging. In the RS primer, Z_cf = φ⁵ lies in (11,12) and appears as the Berry / coherence scale; pinning φ⁵ above 11.09 is the certified floor for that band. The module targets sigma0 DELTA_FORCED (Delta Forcing Spectrum program).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.