phi_cubed_lt
plain-language theorem explainer
The declaration proves that the cube of the golden ratio satisfies φ³ < 4.237. Workers deriving mass ladders or bounding high powers of φ in Recognition Science numerics cite this to cap exponential growth. The proof rewrites the left side via the Fibonacci identity φ³ = 2φ + 1, substitutes the known bound φ < 1.6185, and closes with linear arithmetic.
Claim. Let φ denote the golden ratio (1 + √5)/2. Then φ³ < 4.237.
background
This module supplies rigorous numerical bounds on the golden ratio φ = (1 + √5)/2. It begins from tight inequalities on √5, specifically 2.236 < √5 < 2.237, which imply 1.618 < φ < 1.6185. The local setting is algebraic verification of these bounds to support later power estimates in the phi-ladder.
proof idea
The proof is a one-line wrapper. It rewrites the target using phi_cubed_eq to obtain 2φ + 1 < 4.237, invokes the sibling bound phi_lt_16185 that φ < 1.6185, and finishes with linarith.
why it matters
This result supplies the base cube bound that downstream lemmas such as phi_pow54_lt and phi11_lt in mass verification rely upon. It supports the phi-ladder mass formula by controlling rung growth and appears in the chain of numerical controls that underwrite the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.