phi_pos
plain-language theorem explainer
Positivity of the golden ratio phi follows immediately from its closed-form expression as (1 + sqrt(5))/2. Researchers building the phi-ladder, mass formulas, or the T0-T8 forcing chain in Recognition Science cite this fact to license subsequent inequalities. The tactic proof applies norm_num to seed positivity of 2 and 5, invokes Real.sqrt_pos and add_pos_of_pos_of_nonneg for the numerator, then uses div_pos to conclude.
Claim. Let $phi = (1 + sqrt(5))/2$. Then $0 < phi$.
background
The Constants module supplies elementary facts about the golden ratio phi that appear throughout Recognition Science constructions, including the self-similar fixed point and the phi-ladder mass formula. The module setting anchors all constants to the fundamental RS time quantum tau_0 = 1 tick. The sole upstream dependency is the hypothesis structure that from PhiLadderLattice, which packages a phi-ladder Poisson summation assumption for later discharge but is not invoked in this elementary positivity argument.
proof idea
The tactic proof first obtains 0 < 2 by norm_num. It then proves 0 < sqrt(5) by norm_num on 5 followed by Real.sqrt_pos.mpr. Positivity of the numerator 1 + sqrt(5) is immediate from add_pos_of_pos_of_nonneg. The final step applies div_pos to the numerator and denominator 2, with simpa unfolding the definition of phi.
why it matters
This lemma supplies the minimal positivity fact required for any phi-based inequality in the framework, directly supporting T6 (phi as self-similar fixed point) and the mass formula yardstick * phi^(rung - 8 + gap(Z)). It sits in the Constants module that feeds the eight-tick octave and alpha-band constants. No downstream theorems currently invoke it, leaving it as a foundational but currently isolated closure for the phi-ladder lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.