phi_gt_one
plain-language theorem explainer
The lemma asserts that the golden ratio exceeds one. Workers on the Recognition Science mass ladder or forcing chain cite it to secure the self-similar fixed-point bound. The proof is a direct term reference to the prior algebraic inequality for the golden ratio.
Claim. The golden ratio satisfies $1 < phi$, where $phi = (1 + sqrt(5))/2$.
background
In Recognition Science the golden ratio arises as the unique positive fixed point of the self-similar map in the forcing chain. It satisfies the quadratic equation $phi = 1 + 1/phi$ and is expressed in closed form as $(1 + sqrt(5))/2$. The constants module anchors all RS-native quantities with the fundamental time quantum fixed at one tick. The inequality is first established by comparing square roots of 1 and 5, then lifting the bound through algebraic steps that show 2 is less than 1 plus the square root of 5.
proof idea
The proof is a one-line term wrapper that directly invokes the established inequality for the golden ratio.
why it matters
This alias maintains compatibility across parallel development in the constants section. It supplies the base bound required for the phi-ladder in mass formulas and for the T6 fixed-point step in the forcing chain. The result sits upstream of any derivation that uses phi greater than one in RS-native units where c equals 1 and hbar equals phi to the minus five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.