phi_pow_neg375_upper_hypothesis
plain-language theorem explainer
This definition introduces the external numeric hypothesis that the golden ratio to the power -3.75 is strictly less than 0.165. It is referenced in derivations of upper bounds on tau lepton residues and in the theorem that discharges the hypothesis itself. The declaration consists of a direct definition of the inequality with no reduction steps or lemmas.
Claim. $phi^{-3.75} < 0.165$, where $phi$ is the golden ratio.
background
The module establishes T10 necessity results showing that muon and tau masses are forced from the electron mass (T9) together with geometric constants from cube geometry and the fine-structure constant. The lepton ladder is built from the electron structural mass, step functions involving E_passive = 11, cube faces = 6, wallpaper groups W = 17, alpha, and pi, all combined with the golden ratio fixed point from T4 and the eight-tick octave structure.
proof idea
Direct definition that sets the hypothesis equal to the inequality Real.goldenRatio ^ (-3.75 : ℝ) < (0.165 : ℝ). No lemmas or tactics are invoked.
why it matters
Supplies the hypothesis discharged by phi_pow_neg375_upper_proved (via log bounds on the golden ratio from ElectronMass.Necessity.log_phi_bounds) and used by phi_pow_residue_tau_upper to bound the tau residue. It advances the T10 program of replacing lepton-generation axioms with forced inequalities derived from the phi-ladder and cube geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.