triUniverse_classifier
plain-language theorem explainer
Over a three-claim universe on the golden constraint without positivity, every claim in the law-of-logic closure is classified: the trivial claim is forced, the φ-identification is selected by positivity, and positivity itself is independent (φ versus ψ). Completeness proofs for the maximal-forcing trichotomy cite this. The argument is a three-way case split on the finite claim set, discharging each branch by a named witness.
Claim. For every reality claim $C$ about the three-branch universe, if $C$ lies in the forcing closure generated from the law of logic, then $C$ carries a claim classification (forced, selected, or independent).
background
Maximal forcing classifies reality claims relative to a claim universe and a primitive seed. A claim is in closure when it belongs to the forcing closure of that primitive; here the seed is the law of logic. Classification is a three-way Prop: forced (holds in every admissible realization), selected (resolved by a named selection principle short of full forcing), or independent (two admissible realizations disagree).
This module isolates the Selected branch honestly. The ambient class is the golden-only ratio class $L_{\mathrm{golden}}$: ratios obeying $r^2 = r + 1$ with no positivity cut. Over that class, $r = \varphi$ is not forced, because the conjugate $\psi = (1-\sqrt{5})/2$ satisfies the same algebraic constraint and differs from $\varphi$. Positivity (the physical scale ratio is the expanding root $>1$) is the named principle that selects $\varphi$.
The three-branch universe packages exactly three claims: a trivial claim, the $\varphi$-identification over $L_{\mathrm{golden}}$, and the positivity claim itself. Upstream, InClosure is membership in the forcing closure, and the classification inductive supplies the three constructors used below.
proof idea
Introduce the claim $C$ and the closure hypothesis. Unfold membership in the three-element claim set of the universe (insert/singleton). Case-split on which of the three claims $C$ is.
- Trivial claim: substitute and apply the forced constructor with the already-proved forcedness of the trivial claim.
- $\varphi$-claim: substitute and apply the selected constructor with the positivity selection of $\varphi$ over $L_{\mathrm{golden}}$.
- Positivity claim: substitute and apply the independent constructor with the $\varphi$-versus-$\psi$ independence witness.
No further algebraic work; each branch is a one-line discharge by a sibling lemma.
why it matters
This is the classifier half of the three-branch certificate. Downstream, the maximal-closure certificate for the same universe sets its classifies field to this theorem, and the module-level claim is that a single closure realizes all three trichotomy branches with proofs: one forced, one selected, one independent. That rules out a degenerate classifier that never exercises Selected.
In the broader Recognition forcing story, Forced is already exercised by cost, $\varphi$, dimension, and $\alpha$, and Independent by the mass yardstick. Selected was the missing honest branch. The module also records the drainage path: adopting positivity tightens $L_{\mathrm{golden}}$ to the positive golden class and promotes the $\varphi$-claim to Forced. The classifier itself only tags the three claims; the promotion lemmas sit beside it.
Framework landmarks touched indirectly: T5/T6 force the J-cost and $\varphi$ as the self-similar fixed point, but only after positivity (or an equivalent cut) removes the conjugate. This declaration does not re-derive those; it certifies that the meta-level classification machinery can host that cut as Selected rather than smuggling it into Forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.