phi_pos
plain-language theorem explainer
Phi is strictly positive. Researchers deriving J-cost bounds or phi-ladder mass formulas in Recognition Science cite this fact when establishing non-negativity of costs and geometric-mean optimality. The proof is a short term-mode reduction that unfolds the definition of phi and applies the positivity of the square root of five together with linear arithmetic.
Claim. $0 < phi$ where $phi = (1 + sqrt(5))/2$ is the golden-ratio fixed point of the Recognition Composition Law.
background
In the log-domain J-cost geometry of Recognition Science the canonical cost is $J(x) = 1/2(x + x^{-1}) - 1$ for positive ratios. This module extends core identities from JcostCore to support foundation paper F1, including geometric-mean minimization of total bond cost and the distinction between simultaneous and sequential descent. Phi enters as the self-similar fixed point forced by the Recognition Composition Law. Upstream results define cost as the derivedCost of a multiplicative recognizer comparator and as the J-cost of a recognition event.
proof idea
The proof unfolds the definition of phi, establishes $0 < sqrt(5)$ via Real.sqrt_pos.mpr with a norm_num tactic, and applies linarith to obtain the strict inequality.
why it matters
This positivity result underpins all phi-ladder constructions and mass formulas (T6: phi forced as self-similar fixed point). It supplies the basic arithmetic fact needed for J-cost non-negativity and geometric-mean theorems in the module. Although the head used_by list is empty, the declaration closes a foundational step for the eight-tick octave and D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.