phi_pow_neg9625_upper_v2
plain-language theorem explainer
The inequality bounds the golden ratio to the power of negative 9.625 below 0.00975. Lepton mass modelers in Recognition Science cite it to cap the muon residue term on the phi-ladder. The proof chains a logarithmic lower bound on phi through multiplication by 9.625, exponentiation, inversion, and direct comparison to the target constant.
Claim. $phi^{-9.625} < 0.00975$ where $phi$ is the golden ratio.
background
The module establishes that the lepton ladder is forced from the electron structural mass and constants derived from cube geometry. Masses scale on the phi-ladder as yardstick times phi to the power of (rung minus 8 plus gap). Upstream results include log_phi_bounds supplying the interval (0.481211, 0.481212) for log phi and exp_46316_lower giving exp(4.6316) greater than 102.67. The local setting replaces earlier axioms with explicit bounds on predicted muon and tau masses.
proof idea
The tactic proof invokes log_phi_bounds for the lower bound on log phi. nlinarith produces 4.6316 less than 9.625 times log phi. lt_trans and exp_lt_exp lift this to exp(9.625 log phi) greater than 102.67. Inversion and the identity equating the negative power to the reciprocal yield the upper bound. Final lt_trans compares the result to 0.00975.
why it matters
This bound is consumed by phi_pow_residue_mu_upper_v2 to close the muon residue upper limit. It advances the T10 necessity result that lepton generations follow from the eight-tick octave and phi self-similarity. The result supports the mass formula on the phi-ladder and the alpha inverse interval (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.