phi_pow43_lt
plain-language theorem explainer
The theorem establishes that the golden ratio raised to the 43rd power is strictly less than 970320000. Researchers verifying mass predictions in the Recognition Science framework would cite this bound when checking the proton binding energy interval. The proof decomposes the power into factors whose individual bounds are already established, then multiplies the inequalities while preserving positivity.
Claim. Let $phi = (1 + sqrt(5))/2$. Then $phi^{43} < 970320000$.
background
This module supplies rigorous upper bounds on powers of the golden ratio $phi$ by starting from tight interval bounds on $sqrt(5)$ and hence on $phi$ itself, as described in the module documentation: $2.236 < sqrt(5) < 2.237$ implies $1.618 < phi < 1.6185$, with tighter decimal versions used for higher powers. The relevant prior results are the bounds $phi^3 < 4.237$, $phi^8 < 46.99$, and $phi^{32} < 4873100$, each proved by reducing to the base inequality $phi < 1.6185$ or by recursive decomposition into products of lower powers. These sit inside the broader Recognition Science approach of using the self-similar fixed point $phi$ for scaling relations in the phi-ladder.
proof idea
The proof first rewrites the exponent 43 as 32 + 8 + 3 using ring_nf. It then invokes the three established bounds on $phi^{32}$, $phi^8$, and $phi^3$. Positivity of the higher powers is asserted, after which the product of the first two bounds is formed by mul_lt_mul, the third factor is multiplied in similarly, and the resulting numerical product is shown to lie below 970320000 by norm_num followed by linarith.
why it matters
This bound is invoked directly by the lemma phi43_lt in the mass verification module, which translates it into the statement that the proton binding-energy prediction lies in (969, 970.4) MeV. It therefore supplies one concrete numerical anchor on the phi-ladder used for mass formulas in the Recognition Science framework, consistent with the self-similar fixed point property of $phi$ (T6) and the eight-tick octave structure. No open scaffolding remains here; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.