Lphi0
plain-language theorem explainer
The loosest admissibility class for the phi-layer forcing: every positive real is an admissible candidate scale ratio. Cited whenever one compares the bare positive-ratio universe to the golden-constraint gate, or proves that "r equals phi" is independent before tightening. The body is a one-line structure instance of AdmissibilityClass on the positive reals.
Claim. Define the loose phi-layer admissibility class $L_0^\varphi$ on $\mathbb{R}$ by taking the admissible set to be $\{ r \in \mathbb{R} \mid 0 < r \}$, labeled as positive candidate ratios.
background
This module is Phase 2 of Maximal Forcing: the T6 phi-layer realization. The carrier is a candidate scale ratio $r : \mathbb{R}$. The forced-register pattern from the cost layer is replayed here: a loose class, a gate-tightened class, and a claim under closure that $r$ equals the golden ratio $\varphi$.
An AdmissibilityClass is an abstract pair (admissible set, label) over a realization type $R$. Different phases instantiate $R$ with logic realizations, costed models, or (here) real scale ratios. The companion gate class keeps only positive $r$ that also satisfy the golden constraint $r^2 = r + 1$.
T6 in the forcing chain forces $\varphi$ as the self-similar fixed point. Over the loose positive class that uniqueness is not yet available; the golden gate is what makes the uniqueness theorem apply.
proof idea
Pure structure definition, not a proof. Instantiates AdmissibilityClass on $\mathbb{R}$ by setting the admissible set to the open positive ray ${r \mid 0 < r}$ and fixing the display label. No lemmas are invoked.
why it matters
Baseline of the phi-layer legitimacy argument. Downstream, the tightening from this class to the golden gate is recorded, and effectiveness is proved: the claim "$r = \varphi$" is independent over the positive ray (witnesses $\varphi$ and $1$) but forced once the golden constraint is imposed (wrapping phi_unique_self_similar). That pair is the same style of evidence the cost layer gave for its gate conditions.
Also feeds the phi-universe maximal-closure certificate and the independence theorem that shows the bare positive class does not force $\varphi$. Framework landmark: T6 ($\varphi$ forced by self-similarity); without this loose class one cannot state that the golden gate does real work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.