Phi Support Alternatives Common Constants Fail Selection

Why other constants lose

The golden ratio φ is defined by the equation x² = x + 1, whose positive solution is (1 + √5)/2 ≈ 1.618. This is a classical fact known since antiquity as the extreme and mean ratio, studied by Euclid around 300 BCE. The equation says that a number's square equals the number plus one, a property that links the ratio to self-similarity in geometry, from pentagons to spirals.

What the Recognition Science framework adds is a selection criterion: a formal condition called PhiSelection that picks out exactly one positive real number from all candidates. The criterion is simply that the number must satisfy the same equation x² = x + 1. A machine-checked library of formal theorems proves that the common constants e, π, √2, √3, and √5 all fail this test. For example, π² ≈ 9.870 while π + 1 ≈ 4.142, so π cannot be the solution. The bundle theorem common_constants_fail_selection packages these five exclusions into one statement.

This addresses what the framework calls the numerology objection: the worry that φ was chosen arbitrarily from among nice constants. The theorem shows φ is not one option among many, but the unique positive real satisfying the equation, with the five familiar alternatives ruled out by proof rather than by preference. The framework's library also records a constructive uniqueness result for the positive root, so the selection is forced by the mathematics, not fitted to a desired answer.

The declaration does not claim that these constants are useless or that φ is special in every context. It claims only that they fail this one specific selection criterion. The theorem says nothing about whether e, π, or the square roots appear elsewhere in mathematics or physics, and it does not extend to other constants such as √6 or the Euler-Mascheroni constant, which remain untested by this proof.

/-- 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 does not claim that e, π, or the square roots are mathematically unimportant. The proof does not extend to constants not listed in the bundle theorem. The selection criterion is a definitional choice within the framework, not a universal law of mathematics.

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: