phi_gt_one
plain-language theorem explainer
The golden ratio φ satisfies φ > 1. Any derivation that orders the phi-ladder or invokes positivity of self-similar fixed points in Recognition Science cites this fact. The proof is a one-line wrapper delegating directly to the constant definition in Constants.
Claim. $1 < (1 + 5^{1/2})/2$, where the right-hand side is the golden ratio.
background
The module Inequalities collects basic ordering and positivity facts for the golden ratio φ and the J-cost function. φ is introduced in Constants as the unique positive solution to x² - x - 1 = 0. Upstream lemma one_lt_phi in Constants proves the strict inequality by norm_num on 0 < 2 together with the comparison √1 < √5, which rearranges to 2 < 1 + √5.
proof idea
The proof is a one-line wrapper that applies Constants.one_lt_phi.
why it matters
This ordering anchors all subsequent phi-ladder steps in the forcing chain (T5 J-uniqueness through T6 self-similar fixed point). It is referenced by sibling lemmas such as phi_pos and J_cost_phi inside the same module, ensuring the eight-tick octave and D = 3 constructions remain on the positive reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.