phi_pow_neg377_lower
plain-language theorem explainer
The inequality establishes that the golden ratio to the power -3.77 exceeds 0.163, anchoring a lower bound for the tau lepton residue in forced mass predictions. Researchers deriving lepton generations from the electron mass and cube geometry would cite this numeric fact to close residue intervals. The proof introduces a comparison to 0.164 via norm_num then applies linarith.
Claim. $0.163 < (1 + 5^{1/2})/2)^{-3.77}$
background
This declaration sits inside the T10 module that forces the muon and tau masses from the electron structural mass (T9) together with geometric steps. The golden ratio phi is the self-similar fixed point obtained from the forcing chain (T6). Lepton steps combine E_passive = 11, cube faces = 6, wallpaper count W = 17, and the fine-structure constant alpha derived earlier.
proof idea
One-line wrapper that first proves the auxiliary (0.163 : ℝ) < 0.164 by norm_num, then invokes linarith on the external numeric approximation 0.1638 to obtain the target strict inequality.
why it matters
The bound feeds directly into phi_pow_residue_tau_lower, which supplies the lower estimate for the tau mass prediction interval. It therefore participates in replacing the two original axioms of LeptonGenerations.lean with derived inequalities, completing part of the T10 necessity program that traces lepton masses to the eight-tick octave and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.