phi_lt_onePointEight
plain-language theorem explainer
φ satisfies φ < 1.8. Researchers deriving numerical constraints on the self-similar scale factor in discrete ledgers with J-cost cite this bound when tightening the interval around the golden ratio. The argument is a one-line wrapper that chains the prior result φ < 1.619 through transitivity of < with a direct numerical check that 1.619 < 1.8.
Claim. Let φ = (1 + √5)/2. Then φ < 1.8.
background
The Phi Forcing module shows that self-similarity in a discrete ledger equipped with J-cost forces the scale ratio to satisfy x² = x + 1, hence to equal the golden ratio φ. J is the cost function obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This theorem supplies one link in a chain of real-number bounds that locate φ between 1.6 and 1.8. It depends on the upstream result φ < 1.619, which itself rests on the inequality √5 < 2.238 obtained by comparing squares.
proof idea
The proof applies the transitivity lemma for the less-than relation to the already-proved inequality φ < 1.619 and the numerical fact 1.619 < 1.8. The second comparison is discharged by a norm_num tactic that verifies the floating-point inequality directly.
why it matters
The bound narrows the possible values of the self-similar fixed point forced by the discrete ledger, consistent with T6 of the forcing chain in which φ emerges as the unique positive solution to the self-similarity condition. It forms part of the sequence of inequalities that confirm the numerical location of φ before downstream results connect the ratio to physical constants such as the fine-structure constant. No open questions are closed by this step alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.