Phi Support Lemmas One Lt Phi

The golden ratio's defining inequality

The golden ratio, φ, is the number that satisfies φ² = φ + 1. Its exact value is (1 + √5)/2, approximately 1.618. The declaration one_lt_phi establishes the simple fact that this number is strictly greater than 1. This is not a deep theorem; it follows directly from the closed form, since √5 is greater than 1, making (1 + √5)/2 greater than 1.

This inequality is a foundational building block in the Recognition Science framework, a system that derives physical structure from the mathematics of a ledger, a discrete record of recognition events. The framework's central result proves that any cost function meeting five plain conditions must equal J(x) = (x + 1/x)/2 - 1. From this function, the framework derives the golden ratio as the unique self-similar scaling, and the fact that φ > 1 is a necessary condition for that derivation to make sense as a scaling factor that grows rather than shrinks.

The declaration itself is a lemma, a proven statement within the machine-checked library of formal theorems. It relies on the definition of φ and on Mathlib's pre-existing fact that the golden ratio is greater than 1. Its proof is a direct simplification, not a lengthy argument. In plain terms, it certifies that φ sits on the number line above 1, a position that the rest of the framework's chain of theorems depends on.

What one_lt_phi does not claim is any physical content. It does not say why the golden ratio appears in nature, nor does it assert that any particular object in the universe has proportions equal to φ. It is purely an algebraic statement about the real numbers. The framework's later theorems, which connect φ to physical constants and dimensions, rely on this inequality but are separate claims with their own proofs. This lemma is a support beam, not the building itself.

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

/-- Closed form for φ. -/
lemma phi_def : Constants.phi = Real.goldenRatio := rfl

/-- φ^2 = φ + 1 using the closed form. -/
@[simp] theorem phi_squared : Constants.phi ^ 2 = Constants.phi + 1 := by
  simp [phi_def, Real.goldenRatio_sq]

What this page does not claim

This lemma does not claim any physical or empirical content about the universe. It does not assert that any specific object or process in nature has proportions equal to the golden ratio. It is not a derivation of the golden ratio's importance; it is only a proof that φ > 1.

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: