positivity_promotes_selected_to_forced
plain-language theorem explainer
Over the golden-constraint class without positivity, the claim that the scale ratio equals φ is Selected, not Forced. Adopting positivity as a class tightening promotes that claim to Forced. Anyone tracking the maximal-forcing taxonomy cites this as the explicit drainage of Selected. The proof is a three-component term packing the selection lemma, the tightening witness, and the forced-after-positivity result.
Claim. The claim that the admissible ratio equals $\varphi$ is Selected over the golden-constraint class (ratios $r$ with $r^2=r+1$, no positivity), there exists a Tightening from that class to the golden-plus-positivity class, and the same claim is Forced once positivity is imposed.
background
In the maximal-forcing framework, claims about admissible realizations fall into Forced, Selected, or Independent. This module exercises Selected honestly. The golden-constraint class consists of real $r$ satisfying $r^2=r+1$, without requiring $r>0$. Both $\varphi=(1+\sqrt{5})/2$ and its conjugate $\psi=(1-\sqrt{5})/2$ meet the constraint, so "$r=\varphi$" is not forced over that looser class.
A named selection principle, positivity (the physical scale ratio is the expanding root greater than 1), governs the choice. Tightening records that every realization admissible for a stricter class remains admissible for a looser one: if $r$ is in $B$ then $r$ is in $A$. Adding positivity yields the golden-plus-positivity class, a genuine tightening of the golden-only class. The module setting is Phase 4 of maximal forcing: show the Selected tag and its resolution path in one place.
proof idea
Term-mode proof assembling a triple by constructor. First component: the prior lemma that the phi claim is Selected over the golden-only admissible set (via the positivity selection principle). Second: a nonempty witness of the Tightening structure from golden-only to golden-plus-positivity. Third: the already-proved fact that the phi claim is Forced once positivity is imposed. No tactics beyond packing those three results.
why it matters
Selected must not be a dead end in the Recognition Science forcing taxonomy. The module doc states the point directly: "Selected is not an endpoint... the third branch is never a place a claim goes to die." This theorem is the drainage certificate: positivity as a tightening promotes the phi claim from Selected to Forced, aligning with the T6 landmark that phi is forced as the self-similar fixed point once the right constraints sit on the admissibility class. No downstream dependents are recorded yet; it stands as the Phase 4 witness that the Selected branch has a proved resolution path rather than a perpetual hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.