isPhi_not_forced_over_Lgolden
plain-language theorem explainer
Over the golden-constraint class of ratios (r² = r + 1, no positivity), the claim r = φ is not forced. The conjugate root ψ = (1 − √5)/2 is admissible and differs from φ, so Forced fails. Anyone citing the Selected branch of the maximal-forcing trichotomy needs this negative half. The proof is a pure counterexample: instantiate Forced at ψ and contradict ψ ≠ φ.
Claim. The claim $r = \varphi$ is not forced over the golden-constraint admissibility class (real ratios satisfying $r^2 = r + 1$, with no positivity requirement): it is not true that every admissible $r$ equals $\varphi$.
background
In the maximal-forcing framework, a claim is Forced on an admissible class when it holds for every admissible realization. The claim here is that the scale ratio equals the golden ratio: $r = \varphi$. The class under study is the golden-constraint class: ratios satisfying $r^2 = r + 1$, without the positivity cut $r > 0$. That class is strictly looser than the positive golden class used elsewhere in the phi layer.
The conjugate root $\psi = (1 - \sqrt{5})/2$ (equivalently $1 - \varphi$) satisfies the same quadratic and is the contracting root. Upstream, Forced is the universal quantifier over the admissible set, and the golden-satisfaction lemma for $\psi$ places $\psi$ inside the class. The module's setting is Phase 4 of maximal forcing: an honest exercise of the Selected branch (not Forced, not Independent), with an explicit drainage path once positivity is adopted.
proof idea
Assume Forced holds on the golden-only class for the claim $r = \varphi$. Instantiate the universal quantifier at $\psi$, using that $\psi$ satisfies the golden constraint. This yields $\psi = \varphi$, which contradicts the elementary inequality $\psi \neq \varphi$. The argument is a short term-mode counterexample: intro, apply Forced at the conjugate, discharge by inequality.
why it matters
This is the negative half of the Selected witness for $r = \varphi$ over the golden-only class. Downstream, the companion theorem packages it with the positivity selection principle to obtain Selected status. The module then drains that tag: tightening the class by adding positivity (golden-only to positive-golden) promotes the claim to Forced, recovering the standard forced-phi result. Selected is therefore not a dead end.
In the broader Recognition chain this sits under T6 (phi forced as the self-similar fixed point): the quadratic alone does not pick the expanding root; positivity does. The result keeps the trichotomy honest by showing non-forcedness before the named principle is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.