phi_pow43_gt
plain-language theorem explainer
The inequality 969030000 < φ^43 holds for the golden ratio φ. Mass verification code in the Recognition framework cites this bound to anchor the 43-rung on the phi-ladder for particle masses. The proof decomposes the exponent as 32 + 8 + 3, multiplies the three component lower bounds via mul_lt_mul while tracking positivity, and closes the comparison with norm_num followed by linarith.
Claim. $969030000 < φ^{43}$ where $φ = (1 + √5)/2$ denotes the golden ratio.
background
The module supplies rigorous numerical bounds on powers of the golden ratio φ = (1 + √5)/2. It starts from the elementary inequalities 2.236² < 5 < 2.237², which yield 1.618 < φ < 1.6185, and lifts these to higher powers through algebraic identities such as φ^n = φ^{n-k} · φ^k. Upstream results include phi_pow32_gt establishing 4870400 < φ^32, phi_pow8_gt giving 46.97 < φ^8, and phi_cubed_gt giving 4.236 < φ^3; each reduces to the base phi_gt_1618 bound via ring_nf and linarith.
proof idea
The proof rewrites φ^43 = φ^32 · φ^8 · φ^3 by ring_nf. It invokes phi_pow32_gt, phi_pow8_gt, and phi_cubed_gt to obtain the three lower bounds. Positivity lemmas enable stepwise application of mul_lt_mul to combine them into a single product lower bound. A final norm_num comparison shows the product exceeds 969030000, after which linarith finishes the proof.
why it matters
This bound is invoked by phi43_gt in Masses.Verification after the rewrite Constants.phi = goldenRatio. It supplies a concrete numerical anchor for the phi-ladder mass formula yardstick · φ^(rung - 8 + gap(Z)) and supports proton-mass verification steps tied to the self-similar fixed point of T6. The result closes one link in the chain of exponent bounds required for high-rung checks in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.