sqrt3_fails_selection
plain-language theorem explainer
√3 fails the phi selection criterion because its square equals 3 while √3 + 1 is strictly less than 3. Researchers deriving scaling constants from recognition principles cite this result to exclude common alternatives to the golden ratio. The tactic proof assumes the criterion holds, substitutes the algebraic identity for the square, derives the strict inequality via comparison to √4, and reaches a contradiction with linear arithmetic.
Claim. $¬(√3² = √3 + 1 ∧ √3 > 0)$
background
PhiSelection is the predicate on positive reals x requiring x² = x + 1. This equation selects the unique positive fixed point of the self-similar scaling map in the recognition framework. The Alternatives module proves that several standard constants fail this predicate, addressing the objection that the golden ratio might be an arbitrary choice among familiar numbers.
proof idea
Assume PhiSelection holds for √3. This yields (√3)² = √3 + 1. Replace the left side by the identity (√3)² = 3. Establish √3 < 2 by rewriting as √3 < √4 and applying the square-root monotonicity lemma. Linear arithmetic then shows √3 + 1 < 3. Substituting back produces the contradiction 3 < 3, discharged by linarith after a calc block.
why it matters
The result is invoked by the downstream bundle common_constants_fail_selection, which collects simultaneous failures for e, π, √2, √3 and √5. This supports the claim that φ is the unique positive solution to the selection equation, consistent with the forcing chain step that forces φ as the self-similar fixed point. The module documentation explicitly frames the work as a response to the numerology objection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.