isPhi_selected_over_Lgolden
plain-language theorem explainer
Over the golden-constraint class without positivity, the claim that the scale ratio equals the golden ratio is Selected: not forced, yet governed by a named positivity principle. Anyone citing the maximal-forcing trichotomy or drainage of Selected tags needs this entry. The proof is a two-field term: the prior non-forcing lemma paired with the positivity selection witness.
Claim. The claim $r = \varphi$ is selected over the admissible class of real ratios satisfying the golden constraint $r^2 = r + 1$ (no positivity): it fails to hold in every admissible realization, yet a named selection principle (positivity of the physical scale) governs it.
background
This module exercises the third branch of the maximal-forcing trichotomy. Forced means a claim holds in every admissible realization; Independent means two admissible realizations disagree; Selected means the claim is not forced on the current class but a named selection principle points to one side. Selected is an interim tag that must later drain to Forced or Independent.
The golden-only class consists of real ratios satisfying $r^2 = r + 1$, without requiring $r > 0$. That class is strictly looser than the gate-tightened phi class, which adds positivity. Both roots of the golden equation live in the looser class: $\varphi = (1+\sqrt{5})/2$ and its conjugate $\psi = (1-\sqrt{5})/2$.
The claim under study is simply $r = \varphi$. Upstream, that claim is already Forced on the positive golden class (T6 as a forced invariant, wrapping uniqueness of the self-similar fixed point). Here the ambient class is weaker, so Forced fails and Selected is the honest tag.
proof idea
Selected is defined as the conjunction of non-forcing and a nonempty selection principle. The proof is a pure term constructor of that pair. The first component is the sibling lemma that $r = \varphi$ is not forced over the golden-only class (because $\psi$ is admissible and differs from $\varphi$). The second component packages the named positivity selection principle as a witness of Nonempty. No further tactics or algebraic work.
why it matters
This is the honest Selected witness that completes the trichotomy in the maximal-forcing layer. Downstream, it is the middle conjunct of the non-degeneracy theorem that one closure realizes Forced, Selected, and Independent with proofs, ruling out a secretly always-forced or always-independent classifier. It is also the first conjunct of the drainage theorem: adopting positivity as a tightening of the golden-only class to the positive golden class promotes the claim to Forced, and that promotion is exactly the upstream T6 forcing result. The classifier certificate for the three-claim universe likewise uses this entry for the Selected branch. Framework landmark: T6 (phi forced as the self-similar fixed point) appears here as the resolved endpoint after selection, not as an unmotivated axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.