phi_pow_neg962_upper_proved
plain-language theorem explainer
Physicists deriving muon mass residues in the Recognition Science lepton ladder cite this result to replace an external numeric hypothesis with a verified inequality. It confirms that the golden ratio to the power negative 9.62 is strictly less than 0.0098. The tactic proof obtains tight logarithm bounds on phi, lifts them through exponential monotonicity, and chains the resulting inequalities to the target threshold.
Claim. $phi^{-9.62} < 0.0098$, where $phi$ denotes the golden ratio.
background
The module proves T10 necessity for the lepton ladder, replacing two axioms from LeptonGenerations.lean with bounds on predicted muon and tau masses. These bounds combine the electron structural mass from T9, step functions from cube geometry (E_passive = 11, faces = 6, W = 17), the fine-structure constant, and the golden ratio phi from the self-similar fixed point. The hypothesis phi_pow_neg962_upper_hypothesis encodes the external numeric check required for the muon residue term.
proof idea
The proof unfolds the hypothesis then imports the interval (0.481211, 0.481212) for log(phi) via simpa from log_phi_bounds. Nlinarith produces the comparison 4.62924882 < 9.62 * log(phi); exp_lt_exp lifts it to the exponential side. Lt_trans chains the result to the known lower bound exp_462924882_lower. Inversion, the rpow identity, and exp_neg convert the power form, after which a final transitivity step with the 0.0098 threshold closes the claim.
why it matters
The theorem discharges the hypothesis needed by phi_pow_residue_mu_upper, which supplies the upper bound on the predicted muon residue. This advances the T10 program that forces the lepton ladder from T9 electron mass and the phi fixed point (T6). The eight-tick octave and Recognition Composition Law supply the geometric constants underlying the residue calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.