bottom_strange_ratio_bounds
plain-language theorem explainer
The theorem proves that the golden ratio to the sixth power lies strictly between 17 and 18. Quark mass phenomenologists would cite the result when checking the Recognition Science prediction for the bottom-to-strange quark mass ratio against measured values near 17.9. The proof is a direct one-line application of the already-established sixth-power inequality.
Claim. $17 < phi^6 < 18$, where $phi = (1 + sqrt(5))/2$ is the golden ratio. This supplies the bound on the bottom-to-strange quark mass ratio $m_b/m_s = phi^6$.
background
The module supplies machine-verified numerical predictions for Recognition Science. Each theorem states a rigorous inequality that contains the corresponding experimental value, proved from algebraic identities alone. The golden ratio satisfies $phi^2 = phi + 1$, which yields the Fibonacci identity $phi^6 = 8 phi + 5$ used for generation ratios. The upstream theorem establishes $phi^6 in (17,18)$ by rewriting the sixth power via that identity and applying the bounds $1.5 < phi < 1.62$.
proof idea
The proof is a one-line wrapper that applies the theorem establishing the sixth-power bounds for the golden ratio.
why it matters
The result supplies the proved interval for the bottom-to-strange mass ratio in the module table of RS predictions. It supports the phi-ladder mass formula by confirming that the exponent difference of 6 produces a ratio inside (17,18), consistent with the self-similar fixed point and eight-tick octave structure. No downstream theorems are recorded, so the declaration functions as a terminal numerical anchor for the generation-gap predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.