phi8_lower
plain-language theorem explainer
Certifies the lower rational bracket 46.978 < φ⁸ on the octave rung of the φ-ladder, as an element of ℤ[φ]. Anyone quoting the forced dimensionless mass-ratio φ^k at the eight-tick gap cites this. The proof is a one-line kernel decision of the positivity witness for 1000·φ⁸ − 46978.
Claim. The rational $46978/1000$ lies strictly below $\varphi^8$ in $\mathbb{Z}[\varphi]$: equivalently $0 < 1000\cdot\varphi^8 - 46978$ under the sigma0 positivity predicate on golden integers. Numerically this is the certified lower bound $46.978 < \varphi^8$ (with $\varphi^8 \approx 46.9787$).
background
Recognition Science places every spectral rung on the φ-ladder: two states separated by integer gap $k$ (same yardstick and gap class) stand in the exact dimensionless ratio $\varphi^k$. Here $\varphi$ is the T6 fixed point, and the eight-tick octave (T7) singles out the rung $k=8$.
This module works entirely inside $\mathbb{Z}[\varphi]$ (golden integers). The local power phiPow n is defined by structural recursion so that $\varphi^n = \langle F(n-1), F(n)\rangle$ with Fibonacci coefficients; it reduces under both decide and #eval. The predicate RatLt p q x asserts that the rational $p/q$ lies strictly below $x$, implemented as positivity of the witness $q\cdot x - p$. Positivity itself is the choice-free integer sign test already proved for $s + t\sqrt{5}$ in DeltaSpine.GoldenInt (compare $s^2$ with $5t^2$; a tie is impossible by irrationality of $\sqrt{5}$).
No real square roots, floats, or native_decide appear. The continuum reading is deferred to GoldenIntReal.
proof idea
One-line tactic proof: by decide. After unfolding RatLt and ratWitness, the goal is positivity of the golden integer $1000\cdot\mathrm{phiPow},8 - 46978$. Structural reduction of phiPow 8 yields an explicit Fibonacci pair in $\mathbb{Z}[\varphi]$; clearing to a pure $s+t\sqrt{5}$ form, the kernel compares $s^2$ against $5t^2$ and closes the strict inequality inside {propext, Quot.sound}. No lemmas are invoked by name beyond the decidability instances already attached to IsPos.
why it matters
Feeds the bundled sigma0 certificate ladder_ratio_brackets, which packages lower/upper brackets for $\varphi$, $\varphi^5$, and $\varphi^8$ as a single delta-forced conjunction. That bundle is the arithmetic input to ladder_ratio_real_brackets in GoldenIntReal, which translates the same inequalities into classical real bounds on $\mathrm{PhiForcing}.\varphi^k$ (sigma1, only the $\mathbb{R}$-evaluation costs choice).
Framework landmarks: T6 forces $\varphi$ itself; T7 identifies the eight-tick octave, so $\varphi^8$ is the canonical dimensionless octave ratio on the mass ladder. The module verdict target is sigma0 DELTA_FORCED (audit via scripts/sigma_audit.py), supporting the Delta Forcing Spectrum program. Without this lower bracket the octave half of the forced-ratio thread would be open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.