phiUniverseCert
plain-language theorem explainer
Packages a maximal-closure certificate for the phi-layer claim universe under the law-of-logic primitive. Anyone citing the T6 self-similarity forcing step as a certified closed register needs this object. It is a structure instance that installs the already-proved phi-universe classifier as the classification field.
Claim. There is a maximal-closure certificate for the law-of-logic primitive on the phi-layer claim universe: realizations are real scale ratios $r$ admissible under the golden gate $r>0$ and $r^2=r+1$, the sole claim is "$r=\varphi$", and every claim in the closure is classified.
background
This module is the second concrete maximal-forcing instantiation (Phase 2, T6). The carrier is a candidate scale ratio $r:\mathbb{R}$. The loose class $L_{\varphi0}$ is just the positive reals; the gate class $L_{\varphi\mathrm{Gold}}$ adds the golden constraint $r^2=r+1$. The claim under closure is "$r$ equals the golden ratio $\varphi$".
A MaximalClosureCert for a primitive $P$ and claim universe $U$ is a structure whose single field is a classifier: every reality claim in the closure of $P$ over $U$ receives a ClaimClassification. The phi-layer universe takes realizations in $\mathbb{R}$, admissibility $L_{\varphi\mathrm{Gold}}$, and claim set ${\text{isPhiClaim}}$.
Upstream, phiUniverse_classifier already proves full classification of that universe. Over the gate, "$r=\varphi$" is forced by wrapping PhiForcing.phi_unique_self_similar; over the loose class it is independent ($\varphi$ works, $r=1$ does not).
proof idea
One-line structure instance. The definition builds a MaximalClosureCert for Primitive.lawOfLogic on phiUniverse by setting the classifies field equal to the existing theorem phiUniverse_classifier. No new reasoning: the classifier already shows every claim in the closure equals the singleton claim "$r=\varphi$" and is then classified.
why it matters
Closes the certificate interface for the T6 link of the forcing chain: $\varphi$ as the self-similar fixed point. The module's point is that the forced-register pattern generalizes beyond the cost layer; this definition is the packaged certificate that the phi-layer universe is fully classified under law-of-logic.
It sits beside the independence witness over $L_{\varphi0}$ (phi satisfies the claim, $r=1$ does not), so the golden-constraint tightening does real work, matching the cost-layer legitimacy evidence for gate conditions. No downstream consumers are wired yet in the graph; the object is the reusable cert handle for any later crown or composition theorem that requires a MaximalClosureCert at the phi layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.