PhiSelection
plain-language theorem explainer
PhiSelection isolates the positive real φ satisfying the quadratic φ² = φ + 1. Recognition Science researchers cite it to single out the golden ratio as the unique self-similar fixed point. The definition is a direct conjunction of the algebraic equation and the positivity condition.
Claim. A positive real number $φ$ satisfies the selection criterion when $φ^2 = φ + 1$.
background
This definition sits in the RecogSpec module and encodes the selection criterion for the scaling factor that arises as the self-similar fixed point. The module imports only Mathlib and supplies no upstream lemmas. The predicate therefore stands as the bare mathematical content of the golden-ratio equation.
proof idea
The definition is a direct abbreviation that conjoins the equation φ² = φ + 1 with the strict inequality φ > 0. No lemmas or tactics are applied.
why it matters
The definition supplies the predicate used by the six failure theorems in PhiSupport.Alternatives, which together show that e, π, √2, √3 and √5 all fail the criterion. It thereby implements the T6 step that forces φ as the self-similar fixed point in the unified forcing chain and distinguishes φ from other common constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.