phi_pow6_lt
plain-language theorem explainer
The theorem establishes that the sixth power of the golden ratio satisfies φ^6 < 17.948. Numerics researchers verifying mass formulas on the phi-ladder would cite this bound when computing higher powers such as φ^76. The proof is a one-line reduction that substitutes the algebraic identity φ^6 = 8φ + 5 and applies linear arithmetic to the known upper bound φ < 1.6185.
Claim. $φ^6 < 17.948$ where $φ = (1 + √5)/2$ is the golden ratio.
background
This module supplies rigorous numerical bounds on the golden ratio φ = (1 + √5)/2 using algebraic properties. The local strategy begins with tight bounds on √5, specifically 2.236 < √5 < 2.237, which imply 1.618 < φ < 1.6185. The upstream result phi_lt_16185 states that φ < 1.6185, obtained by unfolding the definition of goldenRatio and applying the bound on √5 via linarith. The companion identity phi_pow6_eq asserts that φ^6 = 8φ + 5, derived from the recurrence relations φ^2 = φ + 1 and φ^4 = 3φ + 2.
proof idea
The proof is a one-line wrapper that first rewrites the left-hand side using the equality phi_pow6_eq, reducing the claim to 8φ + 5 < 17.948. It then invokes linarith on the hypothesis phi_lt_16185 to conclude the inequality by linear arithmetic.
why it matters
This bound supports the computation of higher powers of φ, directly feeding the theorem phi_pow76_lt which establishes φ^76 < 7646046000000000 for proton mass verification. Within the Recognition Science framework it contributes to the phi-ladder used in the mass formula yardstick * φ^(rung - 8 + gap(Z)). It aligns with the self-similar fixed point property of φ at T6 of the forcing chain and enables precise numerical checks against the alpha inverse band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.