IndisputableMonolith.Verification.PhiPinnedCert
Verification certificate that the Recognition Science φ-selection predicate admits exactly one positive real solution. Anyone citing uniqueness of the golden-ratio fixed point in RS units uses this module. The argument packages elementary real-algebra lemmas (square identity, fixed-point form, positive-root uniqueness) around the core selection criterion φ² = φ + 1 with φ > 0.
claimThe RS $\varphi$-selection predicate $\varphi^2 = \varphi + 1$ and $\varphi > 0$ pins a unique real number $\varphi$ (the golden ratio).
background
Recognition Science forces the dimensionless scale factor $\varphi$ as the unique positive solution of the self-similarity equation $x^2 = x + 1$. That equation is the content of the $\varphi$-selection criterion imported from RecogSpec.PhiSelectionCore: $\varphi^2 = \varphi + 1$ together with positivity.
Supporting real-algebra facts live in PhiSupport.Lemmas: the square identity $\varphi^2 = \varphi + 1$ (from Mathlib's golden-ratio API), the fixed-point rewrite $\varphi = 1 + 1/\varphi$, and uniqueness of the positive root of $x^2 = x + 1$. Those lemmas depend only on elementary real arithmetic.
This verification module assembles those pieces into a certificate that the selection predicate determines a single real $\varphi$, the value used throughout the forcing chain (T6) and the mass ladder.
proof idea
Certificate module, not a single theorem body. It imports the selection predicate ($\varphi^2 = \varphi + 1$, $\varphi > 0$) and the golden-ratio support lemmas, then exposes a named certificate object asserting uniqueness of the positive real root. The underlying reasoning is the standard uniqueness argument for the positive root of the monic quadratic $x^2 - x - 1 = 0$, packaged for downstream RS verification consumers.
why it matters in Recognition Science
T6 of the forcing chain requires $\varphi$ to be the unique self-similar fixed point. This module supplies the verification-layer certificate that the RS selection predicate indeed pins that unique real, so later certificates and mass-ladder constructions may treat $\varphi$ as a rigid constant rather than an arbitrary positive scale. No downstream used_by edges are recorded yet; the module stands as a leaf certificate in the Verification domain, ready for import by any proof that needs uniqueness of $\varphi$ without re-deriving the quadratic analysis.
scope and limits
- Does not derive the selection equation itself; that is assumed from PhiSelectionCore.
- Does not address complex or negative roots of $x^2 = x + 1$.
- Does not prove numerical bounds on $\varphi$ beyond uniqueness and positivity.
- Does not connect $\varphi$ to physical constants (c, ħ, G, α); those live elsewhere.
- Does not discharge any sorry; it is a finished certificate module.