OneLtPhiCert
plain-language theorem explainer
Empty certificate tag whose verification predicate is the inequality $1 < \varphi$ for the golden ratio. Anyone needing a named, simp-friendly witness that $\varphi$-powers grow (or that $1/\varphi$ series converge) cites it. The discharge is a one-line wrapper of the Constants lemma `one_lt_phi`.
Claim. There is a certificate type whose verification predicate holds precisely when $1 < \varphi$, with $\varphi = (1 + \sqrt{5})/2$ the golden ratio in RS-native constants. Every inhabitant of the certificate type satisfies that predicate.
background
In Recognition Science the golden ratio $\varphi = (1+\sqrt{5})/2$ is forced as the self-similar fixed point (forcing chain T6). It is the base of the $\varphi$-ladder for masses and the unique minimizer of the J-cost $J(x) = (x + x^{-1})/2 - 1$.
The module packages the elementary lower bound $\varphi > 1$ as a verification certificate. The bound is immediate from $\sqrt{5} > 2$, hence $\varphi > 1.5 > 1$. Upstream, Constants.one_lt_phi proves $1 < \mathrm{phi}$ by comparing square roots and clearing the factor of 2; cosmology and other modules re-export the same fact.
Physically the inequality guarantees ledger balances grow rather than shrink, that geometric series in $1/\varphi$ converge, and that J at $\varphi$ is a minimum rather than a maximum.
proof idea
The structure itself carries no fields; it is a pure tag with Repr. The predicate verified is definitionally the proposition $1 < \mathrm{Constants.phi}$. The theorem verified_any is a one-line wrapper: exact one_lt_phi, invoking the Constants lemma that expands $\varphi = (1+\sqrt{5})/2$ and uses $\sqrt{1} < \sqrt{5}$ plus arithmetic to obtain $1 < \varphi$. Both verified and verified_any are marked @[simp].
why it matters
This is a leaf certificate in the Verification domain: a named, simp-reducible witness for the most basic bound on $\varphi$. The module doc lists the uses that justify packaging it: exponential growth of $\varphi$-powers on the mass ladder, proper J-cost behavior at the T5/T6 fixed point, and convergence of geometric series in $\varphi^{-1}$ (including the dream fraction $\varphi^{-3}$ and related thresholds).
No downstream declarations currently depend on this certificate structure itself (used_by is empty); consumers typically call Constants.one_lt_phi directly. The certificate exists so the verification chain can point at a uniform *.verified interface rather than raw lemmas. It does not advance an open forcing step; it only seals a prerequisite inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.