phi_6_hierarchy_bounds
plain-language theorem explainer
The golden ratio to the sixth power satisfies the strict inequality 17 < φ^6 < 18. This numerical bound is cited when verifying the fermion mass hierarchy prediction in the Recognition Science registry. The proof first invokes the cubic identity φ^3 = 2φ + 1, rewrites the sixth power as a quadratic in φ, and finishes with linear arithmetic on the supplied interval 1.61 < φ < 1.62.
Claim. $17 < φ^6 < 18$, where φ is the golden ratio obeying φ² = φ + 1 and the cubic relation φ³ = 2φ + 1.
background
The Registry Predictions module supplies calculated proofs for items in the COMPLETE_PROBLEM_REGISTRY. It covers the cosmological constant bounds and the fermion mass hierarchy prediction P-002 that relies on the φ^6 and φ^11 structure of the phi-ladder. All proofs employ norm_num, nlinarith and positivity with explicit real bounds.
proof idea
The tactic proof first obtains the cubic identity via phi_cubed_eq. It records the lower bound phi_gt_onePointSixOne and upper bound phi_lt_onePointSixTwo. It then derives φ^6 = (2φ + 1)^2 by nlinarith. The goal is split by constructor and each side is discharged by a separate nlinarith call that uses the interval bounds on φ.
why it matters
This theorem supplies the two φ^6 bounds required by registry_predictions_cert_exists, which constructs an inhabitant of RegistryPredictionsCert by collecting omega_lambda bounds together with these φ^6 facts and the φ^11 lower bound. It directly discharges the P-002 fermion mass hierarchy entry listed in the module documentation. The result is consistent with the mass formula on the phi-ladder and with T6 forcing of phi as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.