PhiNeZeroCert
plain-language theorem explainer
Empty certificate structure whose verification predicate asserts that the golden-ratio constant φ is nonzero. Anyone needing well-defined division by φ, the fixed-point equation φ = 1 + 1/φ, or evaluation of the J-cost at φ would cite it. Discharge is a one-line appeal to the existing positivity lemma for φ.
Claim. There is a certificate type whose verification predicate is the statement $\varphi \neq 0$, where $\varphi = (1+\sqrt{5})/2$ is the golden-ratio constant. Every inhabitant of the certificate type satisfies that predicate.
background
In Recognition Science the golden ratio $\varphi$ is the self-similar fixed point forced by the T6 step of the unified forcing chain. It appears as a scaling base on the $\varphi$-ladder, in the fixed-point identity $\varphi = 1 + 1/\varphi$, and as an evaluation point of the J-cost $J(x) = (x + x^{-1})/2 - 1$. All of those uses require $\varphi \neq 0$ so that division by $\varphi$ is defined.
This module packages that non-degeneracy as a verification certificate. The constant is Constants.phi, identified with Mathlib's Real.goldenRatio. Upstream, PhiSupport.Lemmas.phi_ne_zero already records $\varphi \neq 0$ by reducing to positivity of the golden ratio; Constants.phi_ne_zero is the same fact stated at the constants layer via ne_of_gt phi_pos.
proof idea
The structure itself carries no fields; it is a pure tag type with a Repr instance. The associated predicate verified is definitionally Constants.phi ≠ 0. The discharge theorem verified_any is a one-line wrapper: exact phi_ne_zero, importing the upstream lemma that $\varphi > 0$ (hence $\varphi \neq 0$) from the Mathlib positivity of Real.goldenRatio after unfolding the local definition of $\varphi$.
why it matters
Non-degeneracy of $\varphi$ is a sanity gate for the whole RS constant stack: without it the fixed-point equation forced at T6 is ill-formed, rung arithmetic on the $\varphi$-ladder cannot divide by $\varphi$, and $J(\varphi)$ is undefined. The certificate sits in the Verification domain as a machine-checkable witness that this gate is closed. No downstream consumers are wired in the current graph (used_by is empty), so its role is infrastructural rather than a step inside a larger proved theorem. It closes a basic scaffolding obligation rather than an open research question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.