phi_pow_neg963_lower
plain-language theorem explainer
Recognition Science derivations of the muon mass residue rely on this numeric anchor to bound the phi-powered term below the predicted exponent. It asserts that the golden ratio to the power of negative 9.63 exceeds 0.0097. The short proof uses a norm_num fact to compare the decimal approximations and then applies linarith to close the inequality.
Claim. $0.0097 < phi^{-9.63}$ where $phi$ denotes the golden ratio.
background
In the RRF module on lepton generation necessity, the muon and tau masses are forced from the electron structural mass (T9) together with geometric step functions and the golden ratio phi. The lepton ladder combines E_passive = 11, cube faces = 6, wallpaper groups W = 17, the fine-structure constant alpha, and pi from spherical geometry, all already derived from the eight-tick structure. This particular bound supplies the lower numeric edge for the residue exponent that appears in the predicted muon mass inequality.
proof idea
The proof is a short tactic sequence that first establishes the decimal inequality 0.0097 < 0.00974 by norm_num and then invokes linarith to conclude the desired bound on phi^(-9.63). No upstream lemmas beyond real-number arithmetic are required.
why it matters
This bound feeds directly into phi_pow_residue_mu_lower, which supports the muon mass prediction bounds that replace the earlier axioms in the T10 necessity argument. It anchors the lower end of the phi-ladder residue used to force the muon mass from the electron mass and the step functions. The result closes part of the gap between the geometric constants and the observed lepton spectrum within the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.