pi_fails_selection
plain-language theorem explainer
π does not satisfy the PhiSelection criterion φ² = φ + 1 with φ > 0. Researchers working on the uniqueness of the golden ratio in Recognition Science cite this to exclude common constants. The proof assumes the equation holds for π and derives a contradiction between the bounds π² > 9 and π + 1 < 5.
Claim. The real number π fails to satisfy π² = π + 1 ∧ π > 0.
background
The PhiSelection criterion is the predicate requiring a positive real φ to obey φ² = φ + 1. This equation selects the golden ratio as the unique positive solution. The module proves that common constants including π, e, and square roots of small integers fail this predicate, addressing the objection that φ might be an arbitrary choice among familiar numbers.
proof idea
The proof proceeds by contradiction. Assume PhiSelection holds for π, so π² = π + 1. Apply the Mathlib facts π > 3 and π < 4 to obtain π² > 9 and π + 1 < 5. The resulting chain 9 < π² = π + 1 < 5 yields 9 < 5, which linarith rejects.
why it matters
This result feeds the bundle theorem common_constants_fail_selection, which collects failures for e, π, √2, √3, and √5. The module doc states that the collection shows φ is not an arbitrary choice from among nice constants. It supports the forcing of φ as the self-similar fixed point in the unified chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.