phi43_gt
plain-language theorem explainer
The lemma asserts that 969030000 is strictly less than the golden ratio to the 43rd power. It is cited when bounding the predicted proton binding energy in Recognition Science mass verification against PDG data. The proof is a one-line wrapper that rewrites the Recognition constant to the golden ratio and invokes a precomputed numeric bound.
Claim. $969030000 < phi^{43}$ where $phi$ is the golden ratio identified with the Recognition Science constant.
background
The Masses.Verification module compares RS mass predictions to PDG 2024 experimental values, which are imported as constants rather than derived. The phi-ladder supplies the scaling for these predictions via powers of the golden ratio. Upstream, multiple phi_eq_goldenRatio lemmas establish that Constants.phi equals the mathematical goldenRatio, with one stating 'Constants.phi equals Mathlib's goldenRatio (same definition)'. The module imports interval bounds from Numerics.Interval.PhiBounds.
proof idea
One-line wrapper that rewrites Constants.phi via phi_eq_goldenRatio to goldenRatio, then applies the theorem phi_pow43_gt from Numerics.Interval.PhiBounds.
why it matters
This lemma supports the proton_mass_bounds theorem, which shows the proton binding-energy prediction lies in (969, 970.4) MeV. It fills a step in the machine-verified comparison of RS predictions with PDG data. In the framework it connects to the phi-ladder mass formula and the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.