phi_gt_one
plain-language theorem explainer
The golden ratio exceeds 1, a basic inequality required to index the phi-ladder lattice and guarantee positive spacing on the log scale. Researchers constructing rung indices or applying the Recognition Composition Law cite this fact when verifying lattice points or reciprocal symmetry. The proof unfolds the explicit definition of phi and reduces the claim to a comparison of square roots followed by linear arithmetic.
Claim. Let $phi = (1 + sqrt(5))/2$. Then $1 < phi$.
background
In the phi-ladder lattice module the golden ratio is introduced as the self-similar fixed point forced by Recognition Science theorem T6. The module defines phi explicitly as (1 + sqrt(5))/2 and builds the discrete hierarchy {phi^r : r in Z} on the positive reals, which becomes an additive lattice under the logarithm. This setting supplies the arithmetic progression r * log phi that admits Poisson summation and encodes the eight-tick octave structure of the framework.
proof idea
The tactic proof first unfolds the definition of phi. It then proves the auxiliary claim 2 <= sqrt(5) by rewriting sqrt(4) as 2 via norm_num and the square-root identity, applying monotonicity of the square-root function, and finally invoking linarith to obtain the strict inequality.
why it matters
This inequality is one of the zero-sorry basic facts listed in the module documentation that underpins the entire phi-ladder construction required by T6. It directly enables later results such as log_phi_pos and the reciprocal-symmetry theorems cost_at_phi_pow_eq and cost_phi_ladder_reciprocal. The declaration closes a small scaffolding gap in the discrete hierarchy before the analytic content of PhiLadderPoissonSummation is addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.