phi8_upper
plain-language theorem explainer
Certifies the upper rational bracket φ⁸ < 46979/1000 inside ℤ[φ], with no continuum. Anyone assembling the sigma0 forced-ratio bundle (φ, φ⁵, φ⁸) cites it. The proof is a one-line `decide` on the decidable positivity predicate behind RatGt.
Claim. Writing $\varphi^8$ as the rung-$8$ element of $\mathbb{Z}[\varphi]$, one has $\varphi^8 < 46979/1000$. Equivalently, the rational $46979/1000$ lies strictly above that rung (the decidable integer predicate $0 < p - q\cdot x$ on the witness).
background
The module LadderRatioBounds certifies the forced dimensionless ratio φ and the representative ladder rungs φ⁵, φ⁸ by explicit rational brackets, entirely inside choice-free integer arithmetic on ℤ[φ] (sigma0). The RS mass law places spectrum rungs on the φ-ladder: states separated by rung gap k stand in exact ratio φ^k. φ itself is the T6 self-similar fixed point; φ⁸ is the octave rung (T7 eight-tick period 2³).
phiPow k is φ^k as a structural element of ℤ[φ], reducing under both the kernel and #eval. RatGt p q x means the rational p/q lies strictly above x, defined as positivity of the witness q·x − p via the sigma0 sign predicate IsPos. Because √5-irrationality makes ties impossible (int_sq_eq_five_sq), every concrete bracket is decidable by comparing integer squares, with no Real.sqrt, Float, or native_decide.
The real-side reading of these brackets is deferred to GoldenIntReal (sigma1); only evaluation into ℝ costs Classical.choice.
proof idea
One-line tactic proof: by decide. Unfolding RatGt 46979 1000 (phiPow 8) yields an IsPos goal on an explicit integer witness in ℤ[φ] (equivalently a sign question about s + t√5). Decidability of IsPos plus the already-proved impossibility of s² = 5t² closes the comparison by pure integer arithmetic inside {propext, Quot.sound}. No lemmas are invoked by name; the kernel reduces phiPow 8 and decides the predicate.
why it matters
Fills the upper half of the φ⁸ conjunct in the forced-ratio thread. Downstream, ladder_ratio_brackets packages it with the matching lower bound and the φ, φ⁵ brackets into one sigma0 DELTA_FORCED bundle; ladder_ratio_real_brackets then reads the same arithmetic as genuine real inequalities on the classical golden ratio (σ1 display bridge only).
Framework landmarks: T6 forces φ as the primitive dimensionless ratio; T7 identifies the eight-tick octave, so φ⁸ is the natural rung to pin. The mass formula places states on the φ-ladder with yardstick · φ^(rung−8+gap(Z)); certified brackets on φ⁸ therefore anchor the octave scale without floating-point or continuum hypotheses. Closes a concrete sigma0 obligation in the Delta Forcing Spectrum program: every conjunct here is decide-only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.