phi_lt_onePointSixOneNine
plain-language theorem explainer
The golden ratio satisfies the strict numerical bound φ < 1.619. Researchers bounding the self-similar scale factor in discrete ledgers with J-cost would cite this inequality to chain tighter estimates. The proof reduces the definition of φ, establishes a manual upper bound on √5 by squaring and monotonicity, then closes via linear arithmetic.
Claim. $φ < 1.619$ where $φ = (1 + √5)/2$.
background
The Phi Forcing module shows that self-similarity in a discrete ledger with J-cost forces the scale ratio to satisfy x² = x + 1. The unique positive solution greater than 1 is the golden ratio φ. This numerical bound on φ supports subsequent comparisons in the same module.
proof idea
The proof simplifies the definition of φ. It proves √5 < 2.238 by verifying 5 < (2.238)² with norm_num, rewriting via the square root of a square, and applying sqrt_lt_sqrt. Linear arithmetic then yields the target inequality.
why it matters
This bound is applied directly by lt_trans in the proof of φ < 1.8. It supports the module's main results that self-similar scales equal φ and that discrete ledgers force this ratio, consistent with the T6 step of the Unified Forcing Chain where φ is the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.