sqrt5_pos
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 in Recognition Science
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.
scope and limits
- Does not prove irrationality of √5.
- Does not extend positivity to other algebraic numbers.
- Does not address complex square roots.
- Does not derive numerical approximations.
formal statement (Lean)
62theorem sqrt5_pos : 0 < Real.sqrt 5 := Real.sqrt_pos_of_pos (by norm_num : (5:ℝ) > 0)
proof body
Term-mode proof.
63
64/-- φ > 0 -/