Foundation Logic Real Constants Phi L Gt One

The golden ratio in the framework's own number system

The golden ratio, often written φ, is the number that solves the equation r² = r + 1. Its exact value is (1 + √5)/2, roughly 1.618. The ancient Greeks called it the extreme and mean ratio; it appears in the geometry of the regular pentagon and in the Fibonacci sequence, where each term is the sum of the two before it. A classical fact about φ is that it sits between 1 and 2, and it is irrational, meaning it cannot be written as a fraction of two whole numbers.

In the Recognition Science framework, constants are mirrored onto a special number system called LogicReal. The framework's library of machine-checked formal theorems defines a version of the golden ratio in this system, named phiL, using the same formula: (1 + √5)/2. The declaration phiL_gt_one is a theorem, proved in the machine-checked library, that states this LogicReal version of the golden ratio is strictly greater than 1. The proof works by transporting the statement to the ordinary real numbers, where the corresponding fact about the classical golden ratio is already known, and then carrying the result back.

This theorem is part of a larger effort in the framework to define its physical constants, such as the reduced Planck constant and Newton's gravitational constant, on this recovered real line. The declaration phiL_gt_one is a foundational building block: it establishes a basic ordering property that other proofs can rely on. It does not, by itself, derive any physics. It does not claim that the golden ratio is special because it is greater than one; that is a property shared by countless other numbers. It does not assert that the golden ratio is the only number with this property, nor does it connect the golden ratio to any physical measurement or constant.

What the theorem does establish, within the framework's own formal system, is a simple but necessary fact: the number defined as (1 + √5)/2 is indeed larger than 1. This is a piece of internal bookkeeping that makes the framework's definitions coherent. For a reader outside the framework, the practical takeaway is limited: it is a formal confirmation of a well-known property of the golden ratio, expressed in a specialized number system. The broader claims about what the golden ratio means for physics are separate and are not established by this single declaration.

/-- Recovered φ exceeds 1. -/
theorem phiL_gt_one : (1 : LogicReal) < phiL := by
  rw [lt_iff_toReal_lt, toReal_one, toReal_phiL]
  exact Constants.phi_gt_one

What this page does not claim

This theorem does not derive any physical law or constant. It does not claim the golden ratio is the only number greater than one. It does not establish any connection between the golden ratio and measured physical quantities.

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/Foundation/LogicRealConstants.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: