phi_gt_onePointSix
plain-language theorem explainer
The theorem establishes that the golden ratio φ exceeds 1.6. Researchers tracing the Recognition Science forcing chain cite it when proving that the J-cost of φ is positive. The proof is a one-line term applying transitivity to a numerical comparison and the tighter bound φ > 1.618.
Claim. $φ > 1.6$ where $φ = (1 + √5)/2$ denotes the golden ratio forced by self-similarity.
background
The PhiForcing module shows that a discrete ledger with J-cost structure forces the golden ratio as its self-similar scale ratio. Self-similarity requires that the scale factor x satisfies J(x) = 0 while x ≠ 1, which yields the equation x² = x + 1 whose unique positive root is φ. The Recognition Composition Law supplies the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) that underpins the cost calculations.
proof idea
The proof is a one-line term wrapper: lt_trans (by norm_num) phi_gt_onePointSixOneEight. It chains the numerical fact 1.6 < 1.618 with the upstream result that φ > 1.618.
why it matters
This bound feeds the parent theorem phi_cost_pos, which concludes 0 < J(φ) by linear arithmetic. It sits inside the PhiForcing module that derives φ from self-similarity on a discrete ledger (T6 in the forcing chain) and supplies a convenient numerical anchor before tighter bounds such as φ > 1.618 are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.