Lgolden
plain-language theorem explainer
Admissibility class of real scale ratios obeying the golden constraint r² = r + 1, with no positivity cut. Maximal-forcing work on the Selected branch cites it as the base class where φ is not forced (the conjugate root is admissible) yet is governed by a named positivity principle. Defined as a structure instance packing that set and a label; strictly looser than the positive golden class.
Claim. The admissibility class on $\mathbb{R}$ whose members are exactly the reals $r$ satisfying the golden constraint $r^2 = r + 1$, with no positivity requirement $r > 0$.
background
An admissibility class packages a set of realizations of some abstract type together with a human-readable label. Here the carrier is $\mathbb{R}$, and the set is the solution set of the golden algebraic constraint. That constraint is the self-similarity law for a discrete ledger: scaling by $r$ must compose so that the next scale equals current-plus-base, i.e. $r^2 = r + 1$ (Fibonacci-type recurrence).
The module studies the third branch of the maximal-forcing trichotomy (Forced / Selected / Independent). The golden-only class is the working example: over it, the claim "$r = \varphi$" is not forced, because the conjugate root $\psi = (1-\sqrt{5})/2$ also solves the same equation and differs from $\varphi$.
The positive golden class (positive ratios with the same constraint) is the standard tightening of this class by adding $0 < r$. That tightening is how Selected drains to Forced in the rest of the module.
proof idea
Definitional structure instance, not a proof. The admissible field is the set comprehension ${ r \mid r^2 = r + 1 }$ via the golden-constraint predicate; the label records that positivity is deliberately omitted. No lemmas are applied.
why it matters
This is the base class that makes the Selected branch honest rather than decorative. Over it, "$r = \varphi$" is proved not Forced (conjugate counterexample) and proved Selected under the positivity selection principle; positivity as a tightening then promotes the claim to Forced on the positive golden class. Downstream, it underwrites the non-degeneracy theorem that a single closure realizes all three trichotomy branches (one Forced, one Selected, one Independent), plus the independence of the positivity claim itself and the explicit drainage lemma Selected → Forced.
In the broader framework this sits next to T6 (φ forced as the self-similar fixed point): the algebraic constraint alone does not pick the expanding root; positivity is the named principle that does. The class exists so Selected is never a place a claim goes to die.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.