phi_pow_neg963_lower_proved
plain-language theorem explainer
This theorem proves that the golden ratio raised to -9.63 exceeds 0.0097, discharging the external numeric hypothesis needed for muon residue bounds in lepton generation necessity proofs. Researchers verifying Recognition Science mass predictions from the phi-ladder would cite it when confirming consistency of the muon and tau steps with T9 electron mass. The tactic proof chains log(phi) bounds with exponential inequalities, inversion, and power rewrites to reach the strict lower bound via transitivity.
Claim. The golden ratio satisfies the inequality $phi^{-9.63} > 0.0097$.
background
The T10 module establishes that the muon and tau masses are forced from the electron structural mass (T9) together with step functions drawn from cube geometry, the fine-structure constant, and the golden ratio phi fixed point from T4. This declaration discharges the hypothesis that phi to the power -9.63 exceeds 0.0097, a numeric placeholder required for the predicted residue exponent in the muon mass formula. It draws on upstream log_phi_bounds lemmas (from ElectronMass.Necessity and RSBridge.GapProperties) that place log(phi) inside (0.481211, 0.481212), plus the auxiliary result exp_463407156_upper.
proof idea
The proof unfolds the hypothesis, obtains the log(phi) interval via simpa from ElectronMass.Necessity.log_phi_bounds, and applies nlinarith to reach 9.63 * log(phi) < 4.63407156. It then invokes exp_lt_exp and lt_trans against exp_463407156_upper to bound the exponential, inverts the inequality, rewrites the power via rpow_def_of_pos, ring, and exp_neg, and finishes by transitivity with the numeric fact 0.0097 < 1/103.
why it matters
This result removes an external numeric hypothesis from the lepton ladder forcing argument and feeds directly into phi_pow_residue_mu_lower, which supplies the lower bound for the muon mass prediction. It supports the T10 necessity claim that the lepton rungs are determined by the phi-ladder and eight-tick octave without additional axioms. The step aligns with the Recognition Science chain by confirming consistency of the mass formula yardstick * phi^(rung - 8 + gap(Z)) for the first two lepton generations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.