tighten_Lphi0_LphiGold
plain-language theorem explainer
The golden-constraint class of positive ratios sits inside the unrestricted positive-ratio class: every r with r² = r + 1 is already positive. Builders of the T6 phi-layer maximal-forcing chain cite this as the formal tightening step from the loose carrier to the gate. The body is a one-line projection of the positivity conjunct out of the golden gate predicate, with strictness witnessed by True.
Claim. The admissibility class of positive reals $r$ satisfying the golden constraint $r^2 = r + 1$ is a tightening of the class of all positive reals: every golden-admissible ratio is positive, and the optional strictness witness is taken to be true.
background
This module is the second concrete instantiation of maximal forcing (Phase 2, T6). The carrier is a candidate scale ratio $r : \mathbb{R}$. The loose class is all positive reals; the gate class adds the golden self-similarity constraint $r^2 = r + 1$. Over the gate, $r = \varphi$ is forced by uniqueness of the positive self-similar fixed point; over the loose class it is independent (e.g. $r = 1$ is positive but not golden).
A tightening from class $A$ to class $B$ is the structure whose core field asserts every $B$-admissible realization is $A$-admissible, plus an optional strictness witness (a bare proposition, so the order remains usable before strictness is proved). Here $A$ is the positive-ratio class and $B$ is the golden-gate class built from the predicate that packages positivity with $r^2 = r + 1$.
proof idea
One-line structure instance. The subset field is discharged by introducing a golden-admissible $r$ and projecting the first conjunct of that predicate (positivity), which is exactly membership in the loose positive class. The strictness witness is set to the trivial proposition True; no comparison proof is attempted here.
why it matters
This is the legitimacy edge for the phi layer: it records that the golden gate genuinely narrows the loose positive carrier, the same pattern the cost layer used for its gate conditions. Downstream the module uses the tightened class to force the claim "$r = \varphi$" (wrapping uniqueness of the self-similar fixed point) and to show that same claim is independent over the loose class. In the Recognition forcing chain this is the T6 step: $\varphi$ forced as the self-similar fixed point. No external used-by edges are recorded yet; the declaration is local scaffolding for the phi-universe classifier and the forced-is-phi certificate in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.