phi_pos
plain-language theorem explainer
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
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 φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.