phi_pow_neg375_upper
plain-language theorem explainer
The inequality states that the golden ratio raised to the power -3.75 lies strictly below 0.165 and supplies a numeric upper bound required for the tau lepton residue. Researchers closing the lepton mass predictions under the Recognition Science T10 necessity would cite this result to complete the tau upper limit. The proof is a direct numeric comparison that invokes a decimal approximation followed by linear arithmetic.
Claim. $φ^{-3.75} < 0.165$, where $φ$ denotes the golden ratio.
background
The module proves T10 by showing that muon and tau masses are forced once the electron structural mass from T9 and the geometric constants are fixed. The lepton ladder combines the golden ratio $φ$ (self-similar fixed point from T6) with step functions built from cube geometry (eleven passive edges, six faces, seventeen wallpaper groups), the fine-structure constant, and $π$ from spherical geometry. The exponent -3.75 marks the specific rung position for the tau residue on the $φ$-ladder.
proof idea
The tactic proof first uses norm_num to establish that 0.1639 is less than 0.165, then applies linarith to transfer the inequality directly to the golden ratio power.
why it matters
This bound is invoked by the theorem phi_pow_residue_tau_upper that establishes the upper limit on the predicted tau residue, thereby completing the tau mass bounds required by T10. It anchors the $φ$-ladder rung for the tau generation to the overall forcing chain that begins from the electron mass and the alpha derivation, ensuring the mass formula remains inside observed ranges without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.