Phi Support Lemmas Phi Ne Zero

The nonzero golden ratio

The golden ratio φ is the positive number satisfying φ² = φ + 1, with the closed form (1+√5)/2, approximately 1.618. A basic but essential fact about it is that it is not zero. The declaration phi_ne_zero is a machine-checked proof of exactly this statement: φ ≠ 0. The proof works by showing the golden ratio is positive, since (1+√5)/2 is clearly greater than zero, and a positive number cannot equal zero.

This fact matters because the golden ratio appears in expressions where it sits in a denominator. The fixed-point identity φ = 1 + 1/φ, for instance, requires dividing by φ. Without a proof that φ ≠ 0, that division would be undefined. The lemma phi_ne_zero supplies the necessary guarantee, making later algebraic manipulations legitimate.

The proof relies only on elementary real algebra and the standard definition of the golden ratio. It does not invoke any special framework assumptions. It is a standalone fact about a real number, verified by a computer checking every step of the reasoning.

In Recognition Science, this lemma is a support lemma, a small building block that certificates and later derivations use. The framework's library of formal theorems contains this proof so that when it derives results involving φ, it can safely divide by it. The lemma itself is not a claim about the physical world; it is a statement about the real number φ.

/-- φ ≠ 0. -/
lemma phi_ne_zero : Constants.phi ≠ 0 := by
  -- goldenRatio = (1+√5)/2 ≠ 0
  have : Real.goldenRatio ≠ 0 := by
    have hpos : 0 < Real.goldenRatio := Real.goldenRatio_pos
    exact ne_of_gt hpos
  simpa [phi_def] using this

/-- φ > 1. -/
lemma one_lt_phi : 1 < Constants.phi := by simp [phi_def, Real.one_lt_goldenRatio]

/-- φ = 1 + 1/φ as an algebraic corollary. -/
theorem phi_fixed_point : Constants.phi = 1 + 1 / Constants.phi := by
  have h_sq : Constants.phi ^ 2 = Constants.phi + 1 := phi_squared
  have h_ne_zero : Constants.phi ≠ 0 := phi_ne_zero
  calc
    Constants.phi = (Constants.phi ^ 2) / Constants.phi := by
      rw [pow_two, mul_div_cancel_left₀ _ h_ne_zero]
    _ = (Constants.phi + 1) / Constants.phi := by rw [h_sq]
    _ = Constants.phi / Constants.phi + 1 / Constants.phi := by rw [add_div]
    _ = 1 + 1 / Constants.phi := by
      have : Constants.phi / Constants.phi = 1 := div_self h_ne_zero
      rw [this]

What this page does not claim

The lemma does not claim that the golden ratio is unique as a positive solution to φ² = φ + 1; that is a separate theorem. The lemma does not claim anything about the physical interpretation of the golden ratio in the framework. The lemma does not prove that the golden ratio is irrational or any other number-theoretic property.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/PhiSupport/Lemmas.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: