PhiPinnedCert
plain-language theorem explainer
A unit certificate asserting that the RS φ-selection predicate admits exactly one real solution. Verification and forcing-chain authors cite it to lock the golden-ratio fixed point as the unique admissible scale factor. The proof exhibits Constants.phi, checks the quadratic self-similarity and positivity clauses, then applies the positive-root uniqueness lemma from PhiSupport.
Claim. There is a certificate type whose verification predicate is the statement: there exists a unique real $\varphi$ satisfying the RS $\varphi$-selection condition (positive root of the self-similarity equation $\varphi^2=\varphi+1$). Every inhabitant of the certificate type satisfies that predicate.
background
In Recognition Science the dimensionless scale factor $\varphi$ is not an input constant; it is forced as the unique positive solution of the self-similarity fixed-point equation coming from the J-cost calculus (forcing landmark T6). The predicate PhiSelection packages that algebraic condition together with positivity.
The ambient module is a verification layer: lightweight certificate structures whose verified fields are ordinary propositions, discharged once and for all by simp-friendly theorems. Upstream, PhiSupport supplies phi_squared (the identity $\varphi^2=\varphi+1$ for Constants.phi), one_lt_phi ($1<\varphi$), and phi_unique_pos_root (any positive root of the same quadratic equals $\varphi$). Those three facts are the entire mathematical content needed here.
The certificate itself carries no data; it is a pure marker that the uniqueness claim has been checked in Lean.
proof idea
One-line existence-uniqueness package. Witness is Constants.phi. The PhiSelection constructor is filled by phi_squared (algebraic clause) and by lt_trans of 0<1 with one_lt_phi (positivity clause). Uniqueness is the forward direction of phi_unique_pos_root applied to an arbitrary competitor. The resulting verified_any theorem is marked @[simp], so any later goal of the form PhiPinnedCert.verified _ collapses immediately.
why it matters
Pins the golden-ratio fixed point inside the verification layer, so downstream certificates can treat $\varphi$ as a unique, already-selected real rather than re-proving uniqueness. This is the Lean counterpart of forcing step T6 (φ forced as the self-similar fixed point) and feeds every mass-ladder, eight-tick, and coupling computation that quotes Constants.phi. No downstream consumers are wired yet in the graph (used_by empty), but the certificate is the standard gate that later *Cert bundles import when they need a locked φ. It closes the uniqueness half of the φ-selection obligation; the existence half is already carried by the explicit closed form $(\sqrt{5}+1)/2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.