phi_pos
The declaration shows that the golden ratio φ is positive. Researchers deriving self-similar scales from J-cost ledgers cite it as the initial positivity step before tighter bounds. The tactic proof unfolds the explicit formula for φ, establishes sqrt(5) > 2 via monotonicity of the square root, and closes with linarith.
claim$0 < φ$ where $φ = (1 + √5)/2$ is the positive root of $x^2 = x + 1$.
background
The Phi Forcing module starts from a discrete ledger equipped with J-cost, where the cost function obeys the composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and J(1) = 0. Self-similarity requires that a scale factor x satisfies J(x) = 0 while x ≠ 1, which forces the quadratic x² = x + 1. The positive root of this equation is defined as φ = (1 + √5)/2. The module builds directly on discreteness and ledger axioms to reach this scale factor.
proof idea
The tactic proof first simplifies the definition of φ. It then proves sqrt(5) > 2 by a short calculation: sqrt(5) > sqrt(4) because the square-root function is increasing and 4 < 5, with sqrt(4) = 2. Linarith finishes the proof that (1 + sqrt(5))/2 > 0.
why it matters in Recognition Science
This result supplies the basic positivity fact required for all subsequent inequalities on the self-similar scale in the Phi Forcing module. It supports the chain that begins with the J-cost composition law and ends with φ as the unique positive solution (T6 in the forcing chain). The theorem is a prerequisite for bounds such as φ > 1 and for the main forcing statement that any self-similar discrete ledger must adopt ratio φ.
scope and limits
- Does not prove that φ satisfies the self-similarity equation.
- Does not derive φ from the full ledger axioms.
- Does not relate φ to physical constants such as alpha or G.
formal statement (Lean)
51theorem phi_pos : 0 < φ := by
proof body
Tactic-mode proof.
52 simp only [φ]
53 have h5 : Real.sqrt 5 > 2 := by
54 have h4 : (4 : ℝ) < 5 := by norm_num
55 have hsqrt4 : Real.sqrt 4 = 2 := by
56 rw [show (4 : ℝ) = 2^2 by norm_num, Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
57 calc Real.sqrt 5 > Real.sqrt 4 := Real.sqrt_lt_sqrt (by norm_num) h4
58 _ = 2 := hsqrt4
59 linarith
60
61/-- φ > 1. -/