phi_gt_onePointSixOneEight
plain-language theorem explainer
The theorem asserts that the golden ratio exceeds 1.618. Researchers deriving numerical bounds for the self-similar fixed point in discrete ledgers cite this to anchor coarser estimates such as φ > 1.6. The proof unfolds the definition of φ, establishes a lower bound on sqrt(5) via squaring and monotonicity, then applies linear arithmetic.
Claim. Let $φ = (1 + √5)/2$. Then $φ > 1.618$.
background
The Phi Forcing module derives the golden ratio as the unique positive solution to the self-similarity condition in a discrete ledger with J-cost structure. Self-similar scales satisfy the equation x² = x + 1, and the only x > 0 with J(x) = 0 is x = 1; non-trivial self-similarity therefore forces the scale ratio to φ. The module states that DiscreteLedger L and SelfSimilar L together imply Ratio L = φ.
proof idea
The tactic proof first applies simp to unfold the definition of φ. It then proves sqrt(5) > 2.236 by showing (2.236)² < 5 via norm_num, invoking sqrt monotonicity on the non-negative reals, and rewriting the square root. Linear arithmetic combines the resulting bound with the explicit form of φ to finish the inequality.
why it matters
This bound is used by the coarser theorem φ > 1.6 via transitivity with a numerical comparison. It supports the module's main results that self-similar scales satisfy x² = x + 1 and that φ is the unique positive solution forced by the discrete ledger. In the Recognition Science framework it supplies a concrete numerical anchor for the self-similar fixed point (T6) and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.