phi43_lt
plain-language theorem explainer
The lemma establishes that the golden ratio raised to the 43rd power is strictly less than 970320000. It is cited by researchers checking Recognition Science mass predictions against PDG data. The proof is a one-line term wrapper that rewrites the RS constant to the golden ratio and applies a pre-proven numerical inequality.
Claim. Let $phi$ denote the golden ratio. Then $phi^{43} < 970320000$.
background
The Verification module compares RS-derived mass predictions to PDG 2024 experimental values. For the lepton sector the integer-rung formula is $m = phi^{57+r} / (2^{22} times 10^6)$ in MeV. The constant $phi$ is identified with the mathematical golden ratio in multiple sibling lemmas inside the module and its imports.
proof idea
The term proof first rewrites using the equality that identifies the RS constant with the golden ratio, then applies the exact theorem that bounds the 43rd power by decomposing it into lower powers (32 + 8 + 3) and chaining the corresponding prior inequalities.
why it matters
This lemma is invoked inside the proton_mass_bounds theorem to place the predicted proton binding energy inside the interval (969, 970.4) MeV. It thereby supports verification of the phi-ladder mass formula and the self-similar fixed point from the T6 step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.