all_three_branches_realized
plain-language theorem explainer
A single admissible class (golden-constraint ratios without positivity) simultaneously hosts a Forced claim, a Selected claim, and an Independent claim. Auditors of the maximal-forcing trichotomy cite this as the non-degeneracy certificate: the classifier is not secretly always-forced or always-independent. The proof is a three-component term pairing three already-proved branch witnesses.
Claim. Let $L_{\mathrm{golden}}$ be the class of real ratios satisfying the golden constraint $r^2 = r + 1$, with no positivity requirement. Over this class the trivial claim is forced (holds in every admissible realization), the claim $r = \varphi$ is selected (not forced, but governed by a named selection principle), and a positivity claim is independent (two admissible realizations disagree on it).
background
Maximal forcing classifies reality claims over an admissible class into a trichotomy. Forced means the claim holds for every admissible realization. Independent means two admissible realizations disagree. Selected is the interim tag: the claim is not forced on the current class, yet a named selection principle governs it; the tag must later drain to Forced or Independent by tightening the class.
This module (Phase 4) exercises the Selected branch honestly. The ambient class is $L_{\mathrm{golden}}$: ratios obeying the golden constraint alone, strictly looser than the positive golden class $L_{\varphi\mathrm{Gold}}$. Over $L_{\mathrm{golden}}$, "$r = \varphi$" fails to be forced because the conjugate root $\psi = (1-\sqrt{5})/2$ also satisfies the constraint and differs from $\varphi$. Positivity (the physical scale is the expanding root $> 1$) is the named selection principle that tags the claim Selected and, when adopted as a tightening, promotes it to Forced.
Upstream, Forced, Selected, and Independent are the primitive classifiers; isPhiClaim is the reality claim "$r = \varphi$"; isPhi_selected_over_Lgolden packages non-forcing with the positivity selection principle.
proof idea
Pure term-mode packaging. The proof is the triple constructor applied to three already-established witnesses: trivialClaim_forced (Forced branch), isPhi_selected_over_Lgolden (Selected branch: not forced over $L_{\mathrm{golden}}$, nonempty positivity selection principle), and positiveClaim_independent (Independent branch). No new reasoning; the conjunction is the non-degeneracy statement.
why it matters
Closes the Phase-4 obligation that the third trichotomy branch is live and non-vacuous. Other layers already exercise Forced (cost, phi, dimension, alpha) and Independent (mass yardstick); this module supplies a genuine Selected entry together with its drainage path ($L_{\mathrm{golden}} \to L_{\varphi\mathrm{Gold}}$ promotes "$r = \varphi$" to Forced). The conjunction rules out the failure mode in which the classifier collapses to a single branch.
In the broader Recognition chain this sits under the phi-forcing layer (T6: phi as the self-similar fixed point of the golden constraint). Showing that positivity is a genuine selection step, not a hidden axiom baked into Forced, keeps the forcing ledger honest. No downstream consumers are recorded yet; the result is a completeness certificate for the machinery itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.