triUniverse
plain-language theorem explainer
A single claim universe over the reals whose admissibility class is the golden constraint without positivity, and whose claim set is exactly three: the trivial claim, r equals the golden ratio, and positivity. Anyone citing the three-branch maximal-forcing certificate uses this object as the ambient universe. It is a plain structure instance: Realization is R, admissibility is Lgolden, claims are that finite set.
Claim. Define the three-branch claim universe as the claim universe with realization type $\mathbb{R}$, admissibility class equal to the golden-constraint ratios (satisfying $r^2 = r + 1$, with no positivity requirement), and claim set $\{\text{trivial},\, r = \varphi,\, 0 < r\}$.
background
Maximal forcing classifies each reality claim over an admissibility class into one of three tags: Forced, Selected, or Independent. A claim universe packages a realization type, an admissibility class on that type, and a finite set of claims for one closure pass.
This module's setting is the golden-constraint class without positivity: ratios $r$ with $r^2 = r + 1$. That class admits both $\varphi = (1+\sqrt{5})/2$ and its conjugate $\psi = (1-\sqrt{5})/2$. The tighter class that also requires $0 < r$ is a named tightening of this one. Over the looser class, "$r = \varphi$" is not forced; positivity is the named selection principle that resolves it.
The three packaged claims are: the trivial claim (holds everywhere), the phi claim "$r = \varphi$", and the positivity claim "$0 < r$" (satisfied by $\varphi$, failed by $\psi$). Upstream, ClaimUniverse is the structure being inhabited; Lgolden, isPhiClaim, trivialClaim, and positiveClaim supply the three fields.
proof idea
Definitional structure instance, not a proof. Realization is set to $\mathbb{R}$; admissibility is the golden-constraint class without positivity; claims is the three-element set of the trivial claim, the phi claim, and the positivity claim. No lemmas are applied.
why it matters
This is the ambient universe for the Phase-4 demonstration that the maximal-forcing trichotomy is complete and non-degenerate. Downstream, the classifier theorem shows that over this universe the trivial claim is Forced, the phi claim is Selected (by positivity), and the positivity claim is Independent ($\varphi$ vs $\psi$), using every constructor of the classification. The real certificate packages that classifier for the law-of-logic primitive. The independence witness for positivity is built over this universe ($\varphi$ yes-model, $\psi$ no-model). The drainage theorem (positivity promotes Selected to Forced under the golden-to-positive tightening) is the resolution path that keeps Selected from being a dead end. In the broader RS forcing chain this sits with T5/T6 (J-uniqueness and $\varphi$ as self-similar fixed point): the golden constraint is the algebraic shadow of that fixed point, and positivity is the physical selection of the expanding root.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.