Foundation Logic Real Constants Phi L Pos

The positivity proof

The golden ratio, usually written φ, is the number that solves the equation x² = x + 1. Its exact value is (1 + √5)/2, about 1.618. It appears throughout mathematics: in the regular pentagon, in the Fibonacci sequence, and in the continued fraction [1; 1, 1, 1, ...]. A basic but essential property is that φ is positive, and in fact greater than 1. This is not a deep theorem, but it is a necessary foundation for any further work involving the number.

The declaration phiL_pos is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that the golden ratio, as defined within the framework's own number system, is greater than zero. The proof is short: it shows that the framework's version of φ maps to the standard real number φ, and then uses the already-established fact that the real φ is positive. The framework proves this with no special axioms, relying only on the standard logical foundations of the proof checker.

This positivity result is not an isolated fact. The same file that contains phiL_pos also proves that φ is greater than 1, that it lies between 1.5 and 1.62, and that the framework's version of the reduced Planck constant, ħ, which is defined as φ⁻⁵, falls between 0.088 and 0.093. These bounds are not derived from experiment; they are consequences of the definition of φ and the properties of the number system. The positivity proof is the first step that makes these later bounds possible.

In Recognition Science, the framework models physical constants as derived from a forced cost function, and the golden ratio emerges as the unique self-similar scaling. The phiL_pos theorem does not itself derive any physics. It is a foundational lemma: it establishes a basic property of a number that the framework uses. Without this positivity, statements about the framework's constants would lack a coherent basis. The proof is a piece of internal bookkeeping that keeps the framework's logical structure sound.

What phiL_pos does not claim is important. It does not claim that the golden ratio is physically meaningful in any direct sense, nor that the framework's derivation of φ is complete. It does not assert that the framework's number system is the only way to define real numbers. It simply states a fact about the framework's own definition of φ, and proves it from the definition. The theorem is a small but necessary link in a larger chain, and its value lies in what it enables, not in what it says on its own.

/-- Recovered golden ratio. -/
def phiL : LogicReal :=
  (fromReal 1 + sqrtL (fromReal 5)) / fromReal 2

/-- Positivity of recovered φ. -/
theorem phiL_pos : (0 : LogicReal) < phiL := by
  rw [lt_iff_toReal_lt, toReal_zero, toReal_phiL]
  exact Constants.phi_pos

@[simp] theorem toReal_phiL : toReal phiL = Constants.phi := by
  simp [phiL, Constants.phi, toReal_fromReal]

/-- 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

/-- Recovered lower numerical φ bound. -/
theorem phiL_gt_onePointFive : fromReal (1.5 : ℝ) < phiL := by
  rw [lt_iff_toReal_lt, toReal_fromReal, toReal_phiL]
  exact Constants.phi_gt_onePointFive

/-- Recovered upper numerical φ bound. -/
theorem phiL_lt_onePointSixTwo : phiL < fromReal (1.62 : ℝ) := by
  rw [lt_iff_toReal_lt, toReal_fromReal, toReal_phiL]
  exact Constants.phi_lt_onePointSixTwo

/-- Recovered hbar numerical bounds. -/
theorem hbarL_bounds : fromReal (0.088 : ℝ) < hbarL ∧ hbarL < fromReal (0.093 : ℝ) := by
  constructor
  · rw [lt_iff_toReal_lt, toReal_fromReal, toReal_hbarL]
    exact Constants.hbar_bounds.1
  · rw [lt_iff_toReal_lt, toReal_fromReal, toReal_hbarL]
    exact Constants.hbar_bounds.2

What this page does not claim

The golden ratio is physically meaningful in any direct sense. The framework's derivation of φ is complete or experimentally validated. The framework's number system is the only way to define real numbers. The positivity proof itself derives any physical constant.

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: