phi_pow_11_bounds
plain-language theorem explainer
The theorem proves that the golden ratio to the eleventh power lies strictly between 198 and 200. Researchers deriving quark and lepton mass hierarchies from the phi-ladder in Recognition Science cite this bound to certify the charm-to-up ratio near 199. The proof rewrites the power via the Fibonacci identity and applies linear arithmetic to the tight bounds on phi itself.
Claim. $198 < phi^{11} < 200$, where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The module supplies machine-verified bounds on powers of the golden ratio to match observed mass ratios without floating-point approximation. The phi-ladder formula assigns masses as yardstick times phi to the power (rung minus 8 plus gap(Z)). Upstream phi_pow_11_eq states phi^11 equals 89 phi plus 55 via Fibonacci identities. The constants module supplies the lemmas 1.61 less than phi and phi less than 1.62.
proof idea
The proof rewrites phi^11 using the equality lemma phi_pow_11_eq. It then applies linarith to the lower-bound lemma phi_gt_onePointSixOne and the upper-bound lemma phi_lt_onePointSixTwo to close the interval.
why it matters
This result is invoked directly by charm_up_ratio_bounds to certify m_c/m_u equals phi^11 and by muon_electron_ratio_bounds for m_mu/m_e. It populates the NumericalPredictionsCert structure. In the framework it supports the phi self-similar fixed point (T6) and the mass formula on the phi-ladder, supplying algebraic evidence for the eight-tick octave and D equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.