sqrt5_pos
plain-language theorem explainer
The theorem asserts that the square root of five is positive in the reals. Researchers deriving ordering properties of the golden ratio φ = (1 + √5)/2 in the cost algebra cite it to justify subsequent inequalities. The proof is a one-line term application of the library lemma Real.sqrt_pos_of_pos after norm_num confirms 5 > 0.
Claim. $0 < √5$
background
This result sits in the PhiRing module, which introduces φ := (1 + √5)/2 and its algebraic relations for the J-cost function. The J-cost is given by J(x) = (x + x^{-1})/2 - 1, and the module builds positivity and ordering facts needed for the Recognition Composition Law. No upstream lemmas are required beyond the Mathlib real numbers library.
proof idea
The proof is a direct term-mode wrapper that applies Real.sqrt_pos_of_pos to the fact that 5 > 0, obtained via norm_num.
why it matters
This positivity fact feeds the chain phi_pos, phi_gt_one, phi_inv and J_at_phi, where J(φ) = (√5 - 2)/2 is identified as the minimum nonzero coherence cost on the φ-ladder. It supports the self-similar fixed point (T6) in the forcing chain and the eight-tick octave structure. The result closes a basic scaffolding step for all downstream φ-algebra theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.