golden_ratio_gt_one
plain-language theorem explainer
The lemma establishes that the golden ratio exceeds one. Researchers modeling superfluidity in the Recognition Science framework cite it to confirm the sign of the critical exponent. The short tactic proof first shows the square root of five exceeds one by monotonicity of the square root function applied to one and five, then closes with linear arithmetic.
Claim. $1 < (1 + sqrt(5))/2$
background
The module derives superfluidity from RS eight-tick coherence, treating superfluid He-4 as a BEC of integer-spin bosons and He-3 as Cooper-paired fermions. The golden ratio enters via the phi-ladder and self-similar fixed point in the forcing chain. Upstream results supply the primitive distinctions and simplicial ledger structures that ground the overall derivation from seven axioms to four structural conditions.
proof idea
The tactic proof introduces an auxiliary claim that one is less than the square root of five. This follows by rewriting the square root of one as one and applying the square root monotonicity lemma to the comparison of one and five. Linear arithmetic then combines the auxiliary claim with the target inequality.
why it matters
This lemma supports the theorem rs_critical_exponent_positive, which unfolds the critical exponent and applies logarithm positivity to obtain a strict inequality. It supplies a basic fact required for the superfluidity model in the eight-tick octave framework, where the golden ratio greater than one is presupposed by the self-similar fixed point of T6. The module links to the paper RS_Superfluidity.tex on quantized vortices from U(1) gauge invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.