sqrt2_fails_selection
plain-language theorem explainer
sqrt2_fails_selection establishes that the square root of two fails to satisfy the equation x squared equals x plus one. Researchers confirming the uniqueness of the golden ratio in the Recognition Science framework cite this to exclude common alternatives. The tactic-based proof derives a contradiction by equating the square to two, showing the sum exceeds two, and applying linear arithmetic to reach an impossibility.
Claim. It is not the case that the positive real number satisfying the selection criterion obeys $x^2 = x + 1$ when $x = 2^{1/2}$.
background
The module proves that common mathematical constants fail the PhiSelection criterion, which requires a positive real x to obey x² = x + 1. This addresses the numerology objection by establishing that the golden ratio is the only such number. The upstream result defines PhiSelection (φ : ℝ) as φ² = φ + 1 ∧ φ > 0.
proof idea
Assuming the selection holds gives (√2)² = √2 + 1. The proof invokes Real.sq_sqrt to obtain (√2)² = 2. It then proves 1 < √2 using sqrt_lt_sqrt, deduces √2 + 1 > 2 by linarith, and chains to the contradiction 2 < 2.
why it matters
The theorem is invoked by common_constants_fail_selection, which bundles the failures for exp 1, pi, sqrt 2, sqrt 3, and sqrt 5. This demonstrates that φ is not an arbitrary choice from among nice constants, aligning with the self-similar fixed point forced in the framework. The module doc-comment notes that this shows φ is the only positive real satisfying the selection equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.