phi_pow_neg9627_lower_v2
plain-language theorem explainer
Physicists verifying the forced muon mass in the Recognition Science lepton ladder cite this lower bound on the golden ratio to the power negative 9.627. It ensures the residue calculation stays above the threshold needed for the 2% accuracy claim in T10. The tactic proof chains log bounds through exponential comparison and algebraic rewriting of the power.
Claim. $0.00972 < phi^{-9.627}$ where $phi$ is the golden ratio.
background
The lepton generations necessity module proves T10 by showing muon and tau masses follow from T9 electron mass plus geometric inputs: E_passive = 11 from cube edges, F=6 faces, W=17 wallpaper groups, alpha, and phi. Upstream log_phi_bounds from ElectronMass.Necessity and RSBridge.GapProperties supply the interval (0.481211, 0.481212) for log phi, quoted as 'log(φ) is bounded.' This auxiliary inequality supports residue lower bounds for the predicted muon mass.
proof idea
The proof invokes log_phi_bounds to bound log phi below 0.481212, then applies nlinarith to obtain 9.627 times the log less than 4.6327. It uses lt_trans with exp_46327_upper to bound the exponential below 102.82, takes the reciprocal via one_div_lt_one_div_of_lt, rewrites the power as the reciprocal exponential using rpow_def_of_pos, ring, and exp_neg, and finishes with norm_num plus simpa to chain the numerical lower bound via transitivity.
why it matters
This bound supports the lower estimate for the muon residue in phi_pow_residue_mu_lower_v2, which in turn feeds the muon mass match in lepton_ladder_forced_from_T9. It closes part of the T10 claim that muon and tau masses are determined by electron mass from T9, passive edges 11, faces 6, wallpaper 17, alpha, and phi from T4. In the framework it relies on the self-similar fixed point phi from T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.