Phi Support Alternatives Sqrt2 Fails Selection

Why √2 cannot be the golden ratio

The golden ratio, often written φ, is the positive number that solves the equation x² = x + 1. Its value is (1 + √5)/2, approximately 1.618. The equation means that if you multiply the number by itself, you get the same result as adding 1 to the number. This self-referential property is what makes the golden ratio appear in pentagons, in the Fibonacci sequence, and in many accounts of natural proportions.

The square root of 2, about 1.414, does not have this property. Squaring √2 gives exactly 2, while adding 1 to √2 gives about 2.414. These are different numbers, so √2 fails the defining equation. The same holds for other familiar constants: squaring π gives about 9.87, not about 4.14; squaring e gives about 7.39, not about 3.72. None of them solve x² = x + 1.

Within Recognition Science, this plain arithmetic fact is formalized as a theorem named sqrt2_fails_selection in the framework's machine-checked library of formal theorems. The theorem states that √2 does not satisfy the framework's selection criterion, which is exactly the equation x² = x + 1. The library also proves the same failure for √3, √5, π, and e, and bundles these into a single statement that none of these common constants pass the test. Combined with a separate proof that φ is the unique positive solution, the framework concludes that φ is not chosen by fitting or by preference among nice constants, but is forced by the structure itself.

The theorem does not claim that √2 is useless or that it lacks its own important mathematics. It only establishes that √2 is not the golden ratio. The proof does not involve any empirical measurement, nor does it say anything about whether the golden ratio appears in nature or art. It is a pure statement about real numbers and a specific equation, checked step by step by a computer.

/-- √2 fails the PhiSelection criterion.
    (√2)² = 2 but √2 + 1 ≈ 2.414, so (√2)² ≠ √2 + 1. -/
theorem sqrt2_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 2) := by
  intro h
  have heq : (Real.sqrt 2) ^ 2 = Real.sqrt 2 + 1 := h.left
  -- (√2)² = 2 exactly
  have sqrt2_sq : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)
  -- √2 > 1 (since 2 > 1)
  have sqrt2_gt_one : 1 < Real.sqrt 2 := by
    rw [← Real.sqrt_one]
    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (1 : ℝ) < 2)
  -- So √2 + 1 > 2
  have h2lt : (2 : ℝ) < Real.sqrt 2 + 1 := by linarith [sqrt2_gt_one]
  -- Contradiction: 2 = (√2)² = √2 + 1 > 2
  have : (2 : ℝ) < 2 := by
    calc (2 : ℝ)
        < Real.sqrt 2 + 1 := h2lt
        _ = (Real.sqrt 2) ^ 2 := heq.symm
        _ = 2 := sqrt2_sq
  linarith

/-- Bundle theorem: All tested common constants fail PhiSelection.
    This demonstrates that φ is not an arbitrary choice from among "nice" constants. -/
theorem common_constants_fail_selection :
  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.exp 1) ∧
  ¬IndisputableMonolith.RecogSpec.PhiSelection Real.pi ∧
  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 2) ∧
  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 3) ∧
  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 5) := by
  exact ⟨e_fails_selection, pi_fails_selection, sqrt2_fails_selection,
         sqrt3_fails_selection, sqrt5_fails_selection⟩

/-- √2 fails the PhiSelection criterion.
    (√2)² = 2 but √2 + 1 ≈ 2.414, so (√2)² ≠ √2 + 1. -/
theorem sqrt2_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 2) := by
  intro h
  have heq : (Real.sqrt 2) ^ 2 = Real.sqrt 2 + 1 := h.left
  -- (√2)² = 2 exactly
  have sqrt2_sq : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)
  -- √2 > 1 (since 2 > 1)
  have sqrt2_gt_one : 1 < Real.sqrt 2 := by
    rw [← Real.sqrt_one]
    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (1 : ℝ) < 2)
  -- So √2 + 1 > 2
  have h2lt : (2 : ℝ) < Real.sqrt 2 + 1 := by linarith [sqrt2_gt_one]
  -- Contradiction: 2 = (√2)² = √2 + 1 > 2
  have : (2 : ℝ) < 2 := by
    calc (2 : ℝ)
        < Real.sqrt 2 + 1 := h2lt
        _ = (Real.sqrt 2) ^ 2 := heq.symm
        _ = 2 := sqrt2_sq
  linarith

What this page does not claim

The theorem does not claim that √2 has no mathematical importance or uses. The theorem does not claim that the golden ratio appears in nature or art. The theorem does not involve any empirical measurement or physical observation.

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/Alternatives.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: