phi_cubed_lt
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.
claimLet φ 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 in Recognition Science
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.
scope and limits
- Does not establish a matching lower bound on φ³.
- Does not generalize the bound to arbitrary real exponents.
- Does not verify the bound for complex extensions of φ.
- Does not claim that 4.237 is the tightest possible constant.
Lean usage
have h3 := phi_cubed_ltformal statement (Lean)
304theorem phi_cubed_lt : goldenRatio ^ 3 < (4.237 : ℝ) := by
proof body
Term-mode proof.
305 rw [phi_cubed_eq]
306 have h := phi_lt_16185
307 linarith
308
309/-- φ⁴ = φ³ + φ² = (2φ + 1) + (φ + 1) = 3φ + 2 -/