phi_pow_neg962_upper
plain-language theorem explainer
The bound φ^{-9.62} < 0.0098 supplies an upper limit on the golden ratio power appearing in the muon residue term of the lepton mass ladder. Researchers deriving forced muon and tau masses from T9 electron mass and cube geometry cite it to close the inequality chain. The proof is a short tactic sequence that uses norm_num on the external approximation 0.00974 followed by linarith.
Claim. $φ^{-9.62} < 0.0098$ where $φ$ denotes the golden ratio.
background
The module proves T10 necessity for the lepton ladder, replacing two axioms with derived bounds on predicted muon and tau masses. The ladder is built from the electron structural mass, step functions assembled from E_passive = 11, six cube faces, W = 17 wallpaper groups, α, and π, all combined with the golden ratio φ from T4. This specific numeric bound on φ to the power -9.62 controls the residue contribution in the mass predictions.
proof idea
Tactic proof that first invokes norm_num to establish the concrete comparison 0.00974 < 0.0098, then applies linarith to transfer the inequality to the real power expression.
why it matters
The result is invoked by phi_pow_residue_mu_upper to bound the predicted residue for the muon mass. It supports the module claim that lepton generations are forced by the Recognition Science landmarks (eight-tick octave, phi-ladder, D = 3) without additional axioms. It closes part of the inequality chain required for the full set of lepton mass bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.