sqrt5_fails_selection
plain-language theorem explainer
sqrt5_fails_selection shows that the positive real sqrt(5) fails the quadratic equation x squared equals x plus one that selects the golden ratio. Researchers deriving constants from the Recognition Science forcing chain would cite it to exclude algebraic alternatives from the phi-ladder. The tactic proof assumes the selection property, equates the square to five, derives the strict inequality sqrt(5) plus one less than five, and reaches the contradiction five less than five via linarith.
Claim. The positive real number $x = 5^{1/2}$ does not satisfy $x^2 = x + 1$.
background
The module proves that common constants fail the selection criterion, showing that the golden ratio is the unique positive real solving the quadratic rather than an arbitrary choice. PhiSelection is the predicate requiring a positive real x to obey x squared equals x plus one. The upstream definition states: φ selection criterion: φ² = φ + 1 and φ > 0.
proof idea
The tactic proof proceeds by contradiction. It introduces the assumption that PhiSelection holds for sqrt(5). From the left conjunct it obtains the equation (sqrt 5) squared equals sqrt 5 plus one. Real.sq_sqrt supplies (sqrt 5) squared equals five. A comparison shows sqrt 5 less than three, hence sqrt 5 plus one less than five. The calc block then chains five equals (sqrt 5) squared equals sqrt 5 plus one less than five, producing five less than five. linarith closes the contradiction.
why it matters
The result is invoked by common_constants_fail_selection, which bundles the failures of exp(1), pi, sqrt(2), sqrt(3) and sqrt(5). It fills the module claim that phi is the only positive real satisfying the equation, addressing the numerology objection. Within the framework it reinforces T6 that phi is forced as the self-similar fixed point of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.