PhiSquaredCert
plain-language theorem explainer
Empty audit certificate whose verification predicate asserts the golden-ratio quadratic φ² = φ + 1. Anyone in the RS verification chain who needs the defining algebraic identity of φ cites this package. Discharge is a one-line appeal to the Constants lemma that expands φ = (1+√5)/2 and simplifies.
Claim. There is a certificate type whose verification predicate holds precisely when $\varphi^2 = \varphi + 1$, where $\varphi$ is the golden ratio. Every inhabitant of the certificate type satisfies that predicate.
background
In Recognition Science, φ is the unique positive root of $x^2 - x - 1 = 0$, forced as the self-similar fixed point (forcing-chain T6). The module packages the identity $\varphi^2 = \varphi + 1$ as an audit certificate: an empty structure plus a Prop-valued verification predicate.
Upstream, Constants.phi_sq_eq states the same equality and proves it by substituting $\varphi = (1+\sqrt{5})/2$, using $(\sqrt{5})^2 = 5$, and clearing denominators. A cosmology re-export simply aliases that lemma. The identity implies self-similarity $\varphi = 1 + 1/\varphi$ and the Fibonacci recurrence for powers of φ; every other φ-identity in the stack ultimately rests on it.
proof idea
The structure itself carries no fields. The verification predicate is definitionally the equality $\mathrm{phi}^2 = \mathrm{phi} + 1$. The companion theorem that every certificate is verified is a one-line wrapper: exact phi_sq_eq, i.e. direct application of the Constants lemma that expands the closed form of φ and simplifies by ring arithmetic and the square-root identity.
why it matters
This is the most basic algebraic fact about φ in the RS certificate chain. The module doc calls it the defining equation: it uniquely pins the positive root, yields self-similarity after dividing by φ, and generates the Fibonacci structure of the φ-ladder used in mass formulae and rung arithmetic. Downstream consumers (none linked in the current graph) would use it wherever a verification gate needs a named, simp-friendly witness that φ obeys its quadratic. Framework landmark: T6 (φ forced as self-similar fixed point). No open scaffolding; the underlying lemma is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.