Phi Support Lemmas

The golden ratio's supporting facts

The golden ratio, often written φ, is the positive number satisfying φ² = φ + 1. Its value is (1 + √5)/2, approximately 1.618. This number appears throughout mathematics, from the regular pentagon to the Fibonacci sequence, where successive ratios approach it. A defining property is that φ = 1 + 1/φ: the number is one plus its own reciprocal, which is why it describes self-similar scaling, where a whole relates to its parts the way the parts relate to each other.

Euclid knew this ratio as the extreme and mean ratio, and it has been studied for over two thousand years. The equation x² = x + 1 has two real solutions, one positive and one negative. The positive solution is φ, and the negative solution is its conjugate, approximately -0.618. What makes φ special is not just that it solves the equation, but that it is the only positive solution. This uniqueness is the foundation for any argument that identifies φ as the natural scaling factor in a system that demands self-similarity.

In Recognition Science, the ledger, a discrete record of events, uses φ as its fundamental scaling constant. The framework's library of machine-checked theorems establishes the elementary facts about φ that its larger arguments rely on. The module proves that φ² = φ + 1, that φ = 1 + 1/φ, and that φ is greater than 1 and not zero. These are not new discoveries but formal confirmations of well-known properties, stated in a form the framework can use directly.

The key result is the uniqueness theorem: if any positive number x satisfies x² = x + 1, then x must equal φ. This is proved from the quadratic formula, with no additional assumptions. The theorem is called model-independent because it does not depend on any particular physical model or interpretation; it is a pure fact about real numbers. This means that whenever the framework encounters a positive self-similarity constraint, the golden ratio is the only possible answer, regardless of the context.

These lemmas serve as the groundwork for the framework's more ambitious claims. The self-similarity constraint, when it appears in the forcing chain that derives physical constants, can only be satisfied by φ. The support lemmas make this exclusivity precise and checkable. A reader who wants to verify the framework's reasoning can trace every step back to these elementary facts about the golden ratio, which themselves rest only on standard real algebra.

/-- **Phase 3 Derivation**: Model-independent exclusivity of φ.
    The golden ratio is the unique positive solution to the self-similarity constraint. -/
theorem exclusivity_model_independent :
    ∀ x : ℝ, x > 0 → (x^2 = x + 1) → x = Constants.phi := by
  intro x hx h_eq
  have h_root := phi_unique_pos_root x
  exact h_root.mp ⟨h_eq, hx⟩

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

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

This module does not prove the full forcing chain that derives physical constants from the cost function. The uniqueness theorem does not establish that any physical system must exhibit golden-ratio scaling. The support lemmas do not address the empirical agreement of the framework's predictions with measured values.

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: