common_constants_fail_selection
plain-language theorem explainer
Researchers investigating the forced selection of the golden ratio in Recognition Science cite this result to exclude e, π, √2, √3, and √5 from satisfying the PhiSelection criterion. The declaration rules out common alternatives and thereby supports that φ arises from structure rather than convention. Its term-mode proof is a one-line wrapper that assembles the five individual failure lemmas into a single conjunction.
Claim. The constants $e$, $π$, $√2$, $√3$, and $√5$ each fail the PhiSelection predicate, where PhiSelection encodes the fixed-point equation $x^2 = x + 1$ that selects the golden ratio.
background
This theorem resides in the Alternatives submodule, whose module documentation states that it proves common constants do not satisfy the PhiSelection criterion and thereby shows φ is uniquely determined by mathematical structure rather than arbitrary choice. The local setting directly addresses the numerology objection by exhibiting explicit failures for the listed constants while pairing with the companion uniqueness result for the positive root of $x^2 = x + 1$ (from PhiSupport.lean). PhiSelection is the predicate imported from RecogSpec.PhiSelectionCore that implements the selection properties derived from the Recognition Composition Law and the self-similar fixed point.
proof idea
The proof is a term-mode one-line wrapper. It applies the exact constructor to the five sibling failure theorems e_fails_selection, pi_fails_selection, sqrt2_fails_selection, sqrt3_fails_selection, and sqrt5_fails_selection, packaging their conjunction without further tactics or reductions.
why it matters
The result supplies the exclusion half of the uniqueness argument in the PhiSupport module, reinforcing that φ is the only positive real meeting the selection equation. It feeds the overall claim that φ is mathematically forced (T6) rather than fitted, and it closes one route for the numerology objection within the phi-ladder construction. No open questions remain for this specific bundle, as the theorem is fully proved with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.