Phi Support Alternatives Sqrt3 Fails Selection

The selection test

The golden ratio, φ, is the number that solves the equation x² = x + 1. Its value is (1 + √5)/2, about 1.618. The equation says that squaring the number gives the same result as adding one to it. This single condition is the selection test that Recognition Science applies to candidate scaling constants.

The declaration sqrt3_fails_selection is a machine-checked theorem. It states that √3 does not pass the test. Squaring √3 gives 3, while adding one to √3 gives about 2.732. Because 3 does not equal 2.732, the number √3 cannot play the role that φ plays in the framework's structure. The same exclusion applies to other familiar constants: e, π, √2, and √5 all fail the same test, each for the same reason, their square does not equal the number plus one.

In Recognition Science, the selection equation is not a definitional choice but a consequence of deeper axioms about how recognition events are recorded and priced. The framework's library of formal theorems proves that φ is the only positive real number satisfying x² = x + 1. This uniqueness, combined with the exclusion of common alternatives, answers what the framework calls the numerology objection: φ is not chosen because it looks nice, but because the mathematics leaves no other candidate standing.

The theorem does not claim that √3 is useless or that it never appears in mathematics. It claims only that √3 fails one specific criterion. It also does not claim that the selection equation itself is the deepest principle; the equation is a consequence of the framework's cost function, not a starting assumption. What the theorem changes is the burden of proof: anyone who wants to replace φ with another constant must first show that the replacement satisfies x² = x + 1, and the theorem shows that none of the usual suspects do.

/-- √3 fails the PhiSelection criterion.
    (√3)² = 3 but √3 + 1 ≈ 2.732, so (√3)² ≠ √3 + 1. -/
theorem sqrt3_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 3) := by
  intro h
  have heq : (Real.sqrt 3) ^ 2 = Real.sqrt 3 + 1 := h.left
  have sqrt3_sq : (Real.sqrt 3) ^ 2 = 3 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)
  -- √3 < 2 (since 3 < 4 = 2²)
  have sqrt3_lt_two : Real.sqrt 3 < 2 := by
    have h4 : Real.sqrt 4 = 2 := by norm_num
    rw [← h4]
    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (3 : ℝ) < 4)
  -- So √3 + 1 < 3
  have h3gt : Real.sqrt 3 + 1 < 3 := by linarith [sqrt3_lt_two]
  -- Contradiction: 3 = (√3)² = √3 + 1 < 3
  have : (3 : ℝ) < 3 := by
    calc (3 : ℝ)
        = (Real.sqrt 3) ^ 2 := sqrt3_sq.symm
        _ = Real.sqrt 3 + 1 := heq
        _ < 3 := h3gt
  linarith

/-- √3 fails the PhiSelection criterion.
    (√3)² = 3 but √3 + 1 ≈ 2.732, so (√3)² ≠ √3 + 1. -/
theorem sqrt3_fails_selection : ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 3) := by
  intro h
  have heq : (Real.sqrt 3) ^ 2 = Real.sqrt 3 + 1 := h.left
  have sqrt3_sq : (Real.sqrt 3) ^ 2 = 3 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 3)
  -- √3 < 2 (since 3 < 4 = 2²)
  have sqrt3_lt_two : Real.sqrt 3 < 2 := by
    have h4 : Real.sqrt 4 = 2 := by norm_num
    rw [← h4]
    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (3 : ℝ) < 4)
  -- So √3 + 1 < 3
  have h3gt : Real.sqrt 3 + 1 < 3 := by linarith [sqrt3_lt_two]
  -- Contradiction: 3 = (√3)² = √3 + 1 < 3
  have : (3 : ℝ) < 3 := by
    calc (3 : ℝ)
        = (Real.sqrt 3) ^ 2 := sqrt3_sq.symm
        _ = Real.sqrt 3 + 1 := heq
        _ < 3 := h3gt
  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

The theorem says nothing about whether √3 is useful in other mathematical contexts. The selection equation is not claimed to be a primitive axiom; it is derived from the framework's cost function. The theorem does not prove that φ is the only constant that could ever be relevant, only that these five common ones fail.

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: