phi_11_hierarchy_lower
plain-language theorem explainer
Establishes the bound 180 < phi^11 as a conservative lower limit on the phi-ladder for large fermion mass hierarchies. Cited inside the registry predictions certificate for problem P-002. The term proof rewrites via the Fibonacci identity phi^11 = 89*phi + 55 then closes with linear arithmetic on the lemma phi > 1.61.
Claim. $180 < \phi^{11}$ where $\phi$ is the golden ratio satisfying the Fibonacci identity $\phi^{11} = 89\phi + 55$ and the numerical bound $\phi > 1.61$.
background
The Registry Predictions module supplies calculated proofs for items in the COMPLETE_PROBLEM_REGISTRY, including P-002 on the fermion mass hierarchy with explicit $\phi^6$ and $\phi^{11}$ structure. Masses are assigned on the phi-ladder as yardstick times $\phi$ raised to an integer power offset by gap(Z). Upstream lemma phi_eleventh_eq records the identity "Key identity: $\phi^{11} = 89\phi + 55$ (Fibonacci recurrence)." The companion lemma phi_gt_onePointSixOne supplies the tighter numerical lower bound $\phi > 1.61$.
proof idea
One-line wrapper that rewrites the left-hand side with phi_eleventh_eq then invokes linarith on the hypothesis phi_gt_onePointSixOne.
why it matters
Populates the RegistryPredictionsCert constructor inside registry_predictions_cert_exists, thereby certifying the $\phi^{11}$ hierarchy prediction for P-002. The bound supports the mass formula on the phi-ladder and aligns with T6 where phi is forced as the self-similar fixed point. The module simultaneously certifies the cosmological-constant bounds listed in the same table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.