Phi Support Alternatives Sqrt5 Fails Selection

Why √5 cannot take the role

The golden ratio, φ ≈ 1.618, is the positive number that satisfies x² = x + 1. That equation says the number's square equals the number plus one. It is the defining property that makes φ the self-similar scaling ratio of the five-pointed star and the Fibonacci sequence. A common mathematical neighbor is √5 ≈ 2.236, which appears in the closed form φ = (1 + √5)/2. Because √5 is so close to the golden ratio's construction, one might wonder whether √5 itself could serve the same structural role.

The answer is no, and the framework's machine-checked library of formal theorems makes that precise. The declaration sqrt5_fails_selection proves that √5 does not satisfy the selection criterion x² = x + 1. The arithmetic is plain: (√5)² = 5, while √5 + 1 ≈ 3.236. Since 5 does not equal 3.236, √5 fails the equation outright. The same library proves that e, π, √2, and √3 also fail, and a bundled theorem states that none of these five common constants satisfy the criterion.

In Recognition Science, this exclusion is part of a larger argument that φ is not an arbitrary choice among nice constants. The framework models reality as maintaining a discrete record of recognition events, and from that ledger a cost function is forced by five plain conditions. From that cost function, the golden ratio emerges as the unique positive solution to x² = x + 1. The failure of √5 and the other constants is the negative half of that uniqueness story: it rules out the numerology objection that φ was picked because it looks elegant.

What the declaration does not claim is just as important. It does not say √5 is unimportant; the number remains essential to φ's closed form. It does not say the golden ratio is the only solution to any equation, only to this specific positive-root equation. And it does not by itself prove that φ is the right scaling for the framework's physics. That positive claim comes from the forcing chain that derives φ from the cost function, not from the exclusion of alternatives.

/-- √5 fails the PhiSelection criterion, despite being related to φ.
    (√5)² = 5 but √5 + 1 ≈ 3.236, so (√5)² ≠ √5 + 1.
    Note: φ = (1 + √5)/2, but √5 itself is not the solution. -/
theorem sqrt5_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 5) := by
  intro h
  have heq : (Real.sqrt 5) ^ 2 = Real.sqrt 5 + 1 := h.left
  have sqrt5_sq : (Real.sqrt 5) ^ 2 = 5 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 5)
  -- √5 < 3 (since 5 < 9 = 3²)
  have sqrt5_lt_three : Real.sqrt 5 < 3 := by
    have h9 : Real.sqrt 9 = 3 := by norm_num
    rw [← h9]
    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (5 : ℝ) < 9)
  -- So √5 + 1 < 4 < 5
  have h5gt : Real.sqrt 5 + 1 < 5 := by linarith [sqrt5_lt_three]
  -- Contradiction: 5 = (√5)² = √5 + 1 < 5
  have : (5 : ℝ) < 5 := by
    calc (5 : ℝ)
        = (Real.sqrt 5) ^ 2 := sqrt5_sq.symm
        _ = Real.sqrt 5 + 1 := heq
        _ < 5 := h5gt
  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⟩

What this page does not claim

√5 is not claimed to be mathematically unimportant; it remains essential to the closed form φ = (1 + √5)/2. The exclusion of alternatives does not by itself prove φ is the correct scaling for the framework's physics; that positive claim comes from the forcing chain. The declaration does not claim φ is the only solution to any equation, only to the specific positive-root equation x² = x + 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/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: