PhiAlternativesFailCert
plain-language theorem explainer
Empty certificate tag whose verification predicate asserts that e, π, √2, √3, and √5 each fail the golden-ratio selection rule x² = x + 1 with x > 0. Cited when rebutting the numerology charge that φ is an arbitrary “nice” constant. Discharge is a one-line appeal to the bundled exclusion theorem on those five constants.
Claim. A certificate type whose verification predicate is the conjunction $\neg S(e) \land \neg S(\pi) \land \neg S(\sqrt{2}) \land \neg S(\sqrt{3}) \land \neg S(\sqrt{5})$, where $S(x)$ means $x^2 = x + 1$ and $x > 0$. Any inhabitant of the type satisfies that predicate.
background
In RecogSpec the selection criterion for the self-similar scale is the elementary fixed-point equation $x^2 = x + 1$ together with positivity. That is exactly the algebraic content of the golden ratio $\varphi = (1+\sqrt{5})/2$, and it is the local meaning of T6 in the forcing chain (φ forced as the self-similar fixed point).
This module sits in the Verification layer. Its purpose, stated in the module header, is exclusion rather than uniqueness: show that several textbook constants that look “as nice as φ” fail the same criterion, so φ is not an arbitrary pick among pretty numbers. The companion uniqueness story is the separate PhiPinnedCert path (only one positive root of $x^2 = x + 1$).
The upstream bundle common_constants_fail_selection already proves the five negations for $e$, $\pi$, $\sqrt{2}$, $\sqrt{3}$, and $\sqrt{5}$. The certificate structure is a thin verification wrapper around that bundle.
proof idea
The structure itself is an empty tag (no fields), used only as a certificate carrier. The verified predicate is definitionally the five-way conjunction of failures of the selection criterion on $e$, $\pi$, $\sqrt{2}$, $\sqrt{3}$, and $\sqrt{5}$.
The discharge theorem is a one-line wrapper: it applies the upstream bundle theorem that already establishes exactly that conjunction. No new arithmetic is done at this layer.
why it matters
Addresses the numerology objection head-on. The module header states the intended three-part story: (1) uniqueness of the positive root of $x^2 = x + 1$, (2) exclusion of common alternatives, (3) therefore φ is forced by the selection equation rather than fitted. This declaration is the exclusion half of that pair.
In the Recognition forcing chain this supports T6 (φ as the self-similar fixed point): once the selection equation is accepted, φ is not interchangeable with $e$, $\pi$, or the small square roots, even though φ itself involves $\sqrt{5}$. Downstream consumers of the certificate are not yet wired in this graph (no used_by edges), so the declaration presently stands as a standalone verification artifact rather than a lemma in a larger proof tree.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.