phi_pow_neg963_lower_hypothesis
plain-language theorem explainer
The definition encodes the numeric inequality 0.0097 < golden ratio to the power -9.63 as a named proposition. Researchers closing the muon mass residue bounds in the lepton ladder cite it to replace an earlier axiom. It is introduced directly as a definition of the Prop and discharged by a companion theorem that applies logarithm bounds on the golden ratio.
Claim. The proposition asserts that $0.0097 < 0.0097 < phi^{-9.63}$ holds in the reals, where $phi$ is the golden ratio.
background
The lepton generations module proves that muon and tau masses are forced from the electron mass fixed by T9 together with geometric constants. The ladder is built from the golden ratio phi (T4), cube-derived steps (E_passive = 11, faces = 6, W = 17), and the fine-structure constant alpha. This definition supplies one concrete numeric lower bound required for the predicted muon residue.
proof idea
The declaration is a definition that directly states the inequality (0.0097 : ℝ) < Real.goldenRatio ^ (-9.63 : ℝ). It is a one-line wrapper with no internal tactics. The companion theorem phi_pow_neg963_lower_proved discharges it by unfolding the definition and applying log bounds on the golden ratio.
why it matters
This definition closes the lower bound on the muon residue, which feeds the full T10 necessity result that the three lepton generations are forced. It connects the phi-ladder mass formula to the specific threshold needed once the electron mass and cube geometry are fixed. The result is used by phi_pow_neg963_lower_proved and phi_pow_residue_mu_lower.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.