phi_6_hierarchy_bounds
The declaration proves that 17 is strictly less than the sixth power of the golden ratio while that power remains strictly less than 18. Researchers verifying the phi-ladder predictions for the fermion mass hierarchy in the Recognition Science unification would cite this result. The proof reduces the sixth power via the cubic identity to a quadratic expression and applies linear arithmetic on the supplied numerical interval for phi.
claim$17 < phi^6 < 18$ where $phi$ is the golden ratio satisfying $phi^2 = phi + 1$.
background
This result sits in the module supplying calculated proofs for items in the COMPLETE_PROBLEM_REGISTRY. It addresses the fermion mass hierarchy prediction P-002 by confirming the phi^6 structure. The central identity is phi cubed equals two phi plus one, which follows directly from the Fibonacci recurrence phi squared equals phi plus one. Upstream lemmas supply the tight numerical bounds 1.61 less than phi less than 1.62.
proof idea
The proof invokes phi_cubed_eq to obtain phi cubed equals two phi plus one, then squares the identity to rewrite phi to the sixth as (two phi plus one) squared. It next applies the lower bound from phi_gt_onePointSixOne and the upper bound from phi_lt_onePointSixTwo. Both sides of the target inequality are discharged by nlinarith on the resulting quadratic expression.
why it matters in Recognition Science
The bound is consumed directly by registry_predictions_cert_exists to construct the RegistryPredictionsCert. It supplies the calculated verification for the phi^6 component of the fermion mass hierarchy listed under P-002. Within the framework the result anchors the phi-ladder mass formula and the self-similar fixed point property of phi.
scope and limits
- Does not derive the physical mass formula itself.
- Does not compute explicit particle masses from the hierarchy.
- Does not address the phi^11 lower bound beyond referencing it.
- Does not prove uniqueness of the hierarchy structure.
Lean usage
have h6 := phi_6_hierarchy_boundsformal statement (Lean)
139theorem phi_6_hierarchy_bounds : (17 : ℝ) < (phi : ℝ)^6 ∧ (phi : ℝ)^6 < (18 : ℝ) := by
proof body
Tactic-mode proof.
140 have h3 := phi_cubed_eq -- phi^3 = 2*phi + 1
141 have hphi_lo : phi > 1.61 := phi_gt_onePointSixOne
142 have hphi_hi : phi < 1.62 := phi_lt_onePointSixTwo
143 have h6 : phi^6 = (2 * phi + 1)^2 := by nlinarith [phi_pos]
144 constructor
145 · rw [h6]; nlinarith
146 · rw [h6]; nlinarith
147
148/-- **CALCULATED**: φ^11 > 180 (conservative lower bound for large hierarchies).
149 Uses Fibonacci: phi^11 = 89*phi + 55 > 89*1.618 + 55 > 180. -/