phi5_upper
plain-language theorem explainer
Certifies the upper rational bracket φ⁵ < 11.10 on the φ-ladder, as a choice-free inequality in ℤ[φ]. Anyone citing the forced rung φ⁵ (mass-law yardstick, Z_cf band, Hubble-tension pipeline) uses this bound. The proof is a one-line `decide` on the decidable positivity predicate for the witness 1110 − 100·φ⁵.
Claim. The fifth power of the golden ratio, represented as an element of $\mathbb{Z}[\varphi]$, satisfies $\varphi^5 < 1110/100 = 11.10$. Equivalently, the rational $1110/100$ lies strictly above $\varphi^5$ under the sigma0 ordering on $\mathbb{Z}[\varphi]$.
background
Recognition Science places every spectral rung on the φ-ladder: two states separated by integer gap $k$ stand in the exact dimensionless ratio $\varphi^k$. Here $\varphi$ is the T6 self-similar fixed point, and $\varphi^5$ is the representative rung tied to $Z_{\mathrm{cf}}=\varphi^5\in(11,12)$ and the mass-law yardstick.
This module works entirely inside $\mathbb{Z}[\varphi]$ (GoldenInt). The local power phiPow n is defined by structural recursion (phiPow 0 = 1, phiPow(n+1)=phiPow n · φ), so it reduces under both the kernel and #eval. The predicate RatGt p q x asserts that the rational $p/q$ lies strictly above $x$, implemented as positivity of the integer witness $p - q·x$ via the sigma0 sign predicate IsPos. Decidability follows from comparing integer squares against $5t^2$ (√5-irrationality), with no Real.sqrt, floats, or native_decide.
The module target is sigma0 DELTA_FORCED: every concrete bracket closes inside {propext, Quot.sound}.
proof idea
One-line tactic proof: by decide. Unfolding RatGt 1110 100 (phiPow 5) yields a positivity claim on an explicit element of $\mathbb{Z}[\varphi]$ (equivalently a sign question about $s+t\sqrt{5}$). Because IsPos is a decidable, choice-free integer predicate and phiPow 5 reduces to the concrete Fibonacci pair $\langle 3,5\rangle$ (i.e. $3+5\varphi$), the kernel closes the comparison by pure arithmetic. No lemmas are invoked by name; the decidable instance on RatGt does all the work.
why it matters
Feeds the bundled sigma0 certificate ladder_ratio_brackets, which packages rational brackets for $\varphi$, $\varphi^5$, and $\varphi^8$ (the eight-tick octave rung). That bundle is the arithmetic core of the real-side bridge ladder_ratio_real_brackets in GoldenIntReal, which reads the same inequalities over $\mathbb{R}$ at sigma1.
Downstream, the cosmology pipeline HubbleTensionCert / hubbleTensionCert records a real upper bound $\varphi^5 < 11.11$ as a field of the certificate; this theorem is the sigma0 source of that upper pin. In the RS primer, $\varphi^5$ is the forced constant $Z_{\mathrm{cf}}\in(11,12)$ and appears in the native units $G=\varphi^5/\pi$, $\hbar=\varphi^{-5}$. The bracket is therefore a concrete delta-forced anchor for both the mass ladder and the Hubble-tension channel count.
Closes a pure arithmetic cell of the Delta Forcing Spectrum program; no open scaffold remains on this conjunct.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.