IndisputableMonolith.Foundation.MaximalForcing.RSSelectionExample
Worked example of selection versus forcing at the phi layer. Over a golden-constraint language that admits both roots of $x^2-x-1=0$, the golden ratio is not forced, yet a positivity selector picks it and promotes the selection to a forced claim. Anyone studying Maximal Forcing Phase 2 (T6) or the forced-register pattern would cite it. The argument is definitional setup plus short algebraic and selector lemmas.
claimLet $\psi$ be the conjugate root of the golden equation $x^2-x-1=0$ (so $\psi\neq\varphi$). Let $L_{\mathrm{golden}}$ be the language of positive reals obeying that constraint. Then $\mathrm{isPhi}$ is not forced over $L_{\mathrm{golden}}$, but under a positivity selection it is selected, and positivity promotes that selection to a forced claim.
background
Maximal Forcing packages Recognition Science's forcing chain as a register pattern: a carrier, a loose class of candidates, and successive tightenings that force unique structure. The upstream module RSPhiUniverse is the Phase 2 (T6) realization: the carrier is a scale ratio $r:\mathbb{R}$, and the loose class $L_{\varphi 0}$ is the positive reals, showing the pattern beyond the cost layer.
This module sits one step more concrete. The golden polynomial admits two real roots, $\varphi=(1+\sqrt{5})/2$ and its conjugate $\psi$. A language $L_{\mathrm{golden}}$ that only imposes the golden constraint therefore does not yet single out $\varphi$. The sibling definitions introduce $\psi$, prove $\psi\neq\varphi$, build $L_{\mathrm{golden}}$, and compare it to the tighter phi-gold class.
Selection is the intermediate notion: a criterion (here positivity) that picks one admissible candidate without the full force of the ambient theory. The module then shows how that selection upgrades to forcing once positivity is part of the register.
proof idea
Definitional front half: name $\psi$, record the golden identity and $\psi\neq\varphi$, and define $L_{\mathrm{golden}}$ plus a tightening into the phi-gold class. Middle: prove $\mathrm{isPhi}$ is not forced over $L_{\mathrm{golden}}$ (both roots remain live). Then introduce a positivity selector, show $\varphi$ is selected over $L_{\mathrm{golden}}$, and prove the promotion lemma that positivity turns a selected claim into a forced one. Closing examples (trivialClaim, positiveClaim) illustrate forced versus merely selected status. No deep tactic machinery; short algebraic facts and selector bookkeeping.
why it matters in Recognition Science
Fills the selection gap in the Maximal Forcing story at T6 (phi forced by self-similarity). Upstream, RSPhiUniverse shows the forced-register pattern at the phi layer with loose class the positive reals. This module answers the natural referee question: if one only keeps the golden algebraic constraint, is $\varphi$ already forced? No; the conjugate survives, so forcing needs an extra positivity (or equivalent) cut. That cut is exactly the selection-to-forcing bridge the framework needs before claiming uniqueness of the self-similar fixed point. No downstream Lean dependents are wired yet; the module is an illustrative leaf for the Phase 2 expansion rather than a lemma factory.
scope and limits
- Does not prove full T6 uniqueness of phi in the global forcing chain.
- Does not treat the cost-layer (J) register or RCL identities.
- Does not claim psi is physically realized; it is only a counter-candidate.
- Does not derive numerical constants (c, hbar, G, alpha) from the selection.
- Does not wire downstream theorems; used_by is empty.
depends on (1)
declarations in this module (18)
-
def
psi -
theorem
psi_golden -
theorem
psi_ne_phi -
def
Lgolden -
def
tighten_Lgolden_LphiGold -
theorem
isPhi_not_forced_over_Lgolden -
def
positivitySelection -
theorem
isPhi_selected_over_Lgolden -
theorem
positivity_promotes_selected_to_forced -
def
trivialClaim -
def
positiveClaim -
theorem
trivialClaim_forced -
theorem
positiveClaim_independent -
def
triUniverse -
def
positiveIndepWitness -
theorem
triUniverse_classifier -
def
triUniverseCert -
theorem
all_three_branches_realized