phi_pow_neg377_lower_hypothesis
plain-language theorem explainer
The definition packages the numeric inequality φ^{-3.77} > 0.1629, with φ the golden ratio, as a reusable Prop. Lepton mass derivations in the T10 necessity module cite it to anchor the tau residue lower bound. It is a direct embedding of an external calculation with no internal derivation.
Claim. The proposition stating that $0.1629 < φ^{-3.77}$, where $φ$ is the golden ratio.
background
The module establishes T10 necessity for the lepton ladder, deriving muon and tau masses from the electron structural mass (T9) together with cube geometry steps and the golden ratio φ (T4). Key constants include E_passive = 11, six cube faces, W = 17 wallpaper groups, and α. The definition isolates one numeric bound on φ^{-3.77} that appears in the predicted_residue_tau calculation.
proof idea
Direct definition of the inequality (0.1629 : ℝ) < Real.goldenRatio ^ (-3.77 : ℝ) as a Prop. No lemmas or tactics are applied.
why it matters
It supplies the hypothesis used by phi_pow_neg377_lower_proved and phi_pow_residue_tau_lower, closing part of the T10 argument that the lepton ladder is forced. The bound links to the phi-ladder and eight-tick octave structure. It touches the verification of external numeric constants against derived φ values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.