phi_6_bounds_mass_ratio
plain-language theorem explainer
The theorem proves that the sixth power of the golden ratio lies strictly between 17 and 18. Researchers deriving particle mass ratios from the phi-ladder cite this bound to constrain rung differences. The proof reduces the expression to (2 phi plus 1) squared via the quadratic identity, then closes both sides with nonlinear arithmetic on the interval 1.5 less than phi less than 1.62.
Claim. $17 < phi^6 < 18$ where $phi$ is the golden ratio satisfying $phi^2 = phi + 1$.
background
The module supplies calculated proofs for mass ratios expressed as powers of the golden ratio on the phi-ladder. Upstream lemmas establish the identity phi squared equals phi plus one from the quadratic equation x squared minus x minus 1 equals zero, together with the tighter bounds 1.5 less than phi less than 1.62. These feed the mass scaling convention in RS-native units where masses are real numbers.
proof idea
The proof rewrites phi to the sixth as the square of phi to the third. It substitutes the cubic reduction phi to the third equals 2 phi plus 1 obtained by applying the quadratic identity twice. The lower and upper bounds on phi are then invoked and both directions of the target inequality are settled by nonlinear arithmetic.
why it matters
The bound is used directly by the mass ratio certificate existence theorem in the same module. It anchors a numerical step in the phi-ladder mass formula where ratios arise from rung differences, consistent with the self-similar fixed point forced in the unified chain. No open questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.