phi_lt_two
plain-language theorem explainer
The declaration proves the golden ratio is strictly less than 2. Researchers cite it when bounding stellar mass-to-light ratios and electroweak scales in Recognition Science models. The tactic proof unfolds the explicit algebraic definition of the golden ratio, reduces the claim to a square-root comparison via monotonicity, and resolves it with linear arithmetic.
Claim. Let $phi = (1 + sqrt(5))/2$. Then $phi < 2$.
background
The Recognition Entropy module develops information measured in phi-bits, with CP6 channel capacity scaling as phi to the 12 rather than base-2 Shannon bits. The golden ratio arises as the self-similar fixed point in the forcing chain and satisfies the quadratic equation x squared equals x plus 1. Upstream lemmas in Constants and PhiForcing establish the same bound through norm_num and square-root comparisons.
proof idea
Unfold the definition of the golden ratio. Establish sqrt(5) less than 3 by rewriting 3 as sqrt(9) and applying the square-root inequality for positive reals. Conclude directly with linarith.
why it matters
This bound is invoked in downstream results on nucleosynthesis mass-to-light ratios matching observations and the electroweak VEV phi window. It supports the claim that each phi-bit carries more discrimination than a binary bit, consistent with the recognition composition law and the eight-tick octave. The inequality closes a basic prerequisite for capacity comparisons in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.