LphiGold
plain-language theorem explainer
Gate-tightened admissibility class of positive real scale ratios that obey the golden equation r^{2} = r + 1. It is the carrier over which T6 forces the candidate ratio to equal phi. Anyone citing the phi-layer forcing or the Lphi0-to-gate tightening uses this class. The body is a one-line packaging of the PhiAdmissible predicate into an AdmissibilityClass.
Claim. Let $L_{\phi}^{\mathrm{Gold}}$ be the admissibility class on $\mathbb{R}$ whose admissible set is $\{ r \in \mathbb{R} : 0 < r \text{ and } r^2 = r + 1 \}$, labeled as positive ratios with the golden constraint.
background
This module is Phase 2 of Maximal Forcing: the phi-layer realization of the forced-register pattern at T6 (phi forced by self-similarity). The carrier is a candidate scale ratio $r : \mathbb{R}$. The loose class is just the positive reals; the gate class adds the golden constraint.
An AdmissibilityClass is an abstract pair (admissible set, label) over a realization type $R$. Here $R = \mathbb{R}$. The predicate packaged into the set is positivity plus the golden equation $r^2 = r + 1$ (the self-similarity fixed-point condition from the forcing chain).
The looser sibling class keeps only $0 < r$. The contrast between the two classes is the legitimacy test for the gate: the claim "$r = \varphi$" is independent over positives alone and forced once the golden constraint is imposed.
proof idea
Definitional packaging, not a proof. The admissible field is the set comprehension of the phi-layer admissibility predicate (positive and satisfies the golden constraint). The label string records that reading for display. No tactics or lemmas are applied.
why it matters
This is the gate class for the T6 phi-layer. Downstream, the claim universe is built with this class as its admissibility, and "r equals phi" is proved forced over it by wrapping the unique-self-similar fixed-point theorem from PhiForcing. The same class appears in the tightening from the loose positive class, and in the effectiveness theorem that the golden constraint is legitimate: independence over positives, forced over the gate.
In the Recognition chain this is the concrete T6 register: phi as the self-similar fixed point. Selection examples outside the module also reuse the class as the golden admissibility layer. Without it there is no gate against which to measure that the tightening does real work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.