phi_gt_one
plain-language theorem explainer
The inequality phi > 1 establishes that the golden ratio exceeds unity, a prerequisite for defining logarithms in base phi for recognition entropy. Researchers modeling CP6 channel capacity in phi-bits would cite it to ensure the information measure is positive and well-defined. The tactic proof unfolds the algebraic definition of phi and reduces the claim to a square-root comparison via linarith.
Claim. Let $phi = (1 + sqrt(5))/2$. Then $phi > 1$.
background
The Recognition Entropy module measures information in phi-bits (log base phi) rather than Shannon bits, with CP6 recognition capacity scaling as phi^12. Phi enters as the self-similar fixed point from the forcing chain, calibrated by J-cost structures and the active edge count A at D=3. Upstream results supply the nuclear density tiers, ledger factorization for J, and spectral emergence of gauge content that together fix the phi-ladder.
proof idea
The tactic proof unfolds the definition of phi, proves an auxiliary fact that sqrt(5) > 1 by rewriting 1 as sqrt(1) and invoking sqrt_lt_sqrt with norm_num, then closes with linarith.
why it matters
This result supplies the basic positivity needed for phi-bit definitions and recognition entropy calculations, supporting downstream comparisons of recognition capacity against Shannon limits. It closes a prerequisite in the phi-forcing layer, consistent with the eight-tick octave and D=3 in the unified chain. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.