phi_lt_onePointEight
plain-language theorem explainer
The golden ratio satisfies φ < 1.8. Researchers tracing the Recognition Science forcing chain cite this bound when numerically constraining the self-similar scale factor that emerges from J-cost self-similarity. The proof is a one-line wrapper that chains a tighter prior bound through order transitivity and a direct numerical check.
Claim. The golden ratio satisfies $φ < 1.8$.
background
The PhiForcing module establishes that self-similarity on a discrete ledger equipped with J-cost forces the scale ratio to satisfy the golden-ratio equation x² = x + 1, with φ the unique positive solution. The local setting begins from a discrete ledger whose cost structure is invariant under rescaling, so that J(x) = 0 only for the trivial scale x = 1; nontrivial self-similarity therefore selects the fixed point of the recurrence. Upstream, phi_lt_onePointSixOneNine supplies the tighter bound φ < 1.619 by explicit comparison of √5 against a rational square, while lt_trans supplies the transitivity step used to lift that bound.
proof idea
One-line wrapper that applies lt_trans to phi_lt_onePointSixOneNine together with a norm_num verification that 1.619 < 1.8.
why it matters
The inequality belongs to the family of numerical bounds that close the self-similarity argument in PhiForcing, confirming that the forced scale lies inside the interval required by the Recognition Science forcing chain (T6: phi forced as the self-similar fixed point). It supplies concrete numerical control that later steps in the module can invoke when comparing φ against other constants derived from the same ledger. No direct downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.