phi_cubed_gt
plain-language theorem explainer
The inequality 4.236 < φ³ holds for the golden ratio φ. Mass verification routines and higher-power bound constructions cite this cubic anchor to control the phi ladder. The proof rewrites the cubic via the Fibonacci identity φ³ = 2φ + 1 then closes the inequality by linear arithmetic on the established lower bound φ > 1.618.
Claim. $4.236 < φ^3$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies rigorous numerical bounds on φ by sandwiching √5 between 2.236 and 2.237, which immediately yields 1.618 < φ < 1.6185. The cubic identity φ³ = 2φ + 1 is obtained from the defining relation φ² = φ + 1 by multiplication and rearrangement. Upstream results supply both the identity (phi_cubed_eq) and the base inequality φ > 1.618 (phi_gt_1618).
proof idea
The proof is a one-line wrapper. It rewrites the left-hand side using the cubic identity φ³ = 2φ + 1, imports the lower bound φ > 1.618, and closes the inequality by linear arithmetic.
why it matters
This bound feeds the verification of φ¹¹ > 198.9 in mass calculations and the construction of higher powers such as φ⁴³ and φ⁵⁴. It anchors the phi-ladder inequalities required for mass formulas and resonance calculations. The result closes a gap in the chain of bounds needed for self-similar fixed-point applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.