IndisputableMonolith.Foundation.MaximalForcing.RSSelectionExample
Worked example of selection versus forcing at the phi layer: the golden conjugate is admissible under a loose golden constraint, so uniqueness of phi fails, yet a positivity selection rule restores phi as the unique selected (and then forced) scale. Anyone studying T6 self-similarity or the forced-register pattern would cite it. The argument is a short chain of concrete real-analysis facts plus one selection-to-forcing promotion lemma.
claimLet $\psi = (1-\sqrt{5})/2$ be the golden conjugate and $L_{\mathrm{golden}}$ the class of positive reals satisfying the golden algebraic constraint. Then $\psi \neq \varphi$, $\mathrm{IsPhi}$ is not forced over $L_{\mathrm{golden}}$, but under the positivity selection rule $\mathrm{IsPhi}$ is selected over $L_{\mathrm{golden}}$, and positivity promotes that selection to a forced claim.
background
This module sits in the Maximal Forcing stack as a selection example on top of the phi-layer realization. Upstream, RSPhiUniverse is the Phase-2 expansion of T6: the carrier is a candidate scale ratio $r \in \mathbb{R}$, and the loose class is the positive reals, showing that the forced-register pattern extends from the cost layer to self-similar forcing of $\varphi$.
Here the golden constraint is deliberately loosened so both roots of the golden equation are a priori admissible. The conjugate $\psi = (1-\sqrt{5})/2$ is introduced as that second root; $L_{\mathrm{golden}}$ is the corresponding loose class. Selection (positivity) is the extra filter that discards the negative conjugate and restores uniqueness of $\varphi$.
Notation follows the forced-register pattern: a claim is forced over a class when every member satisfies it; it is selected when a named selection rule singles it out; positivity is the rule that keeps only positive scales.
proof idea
The module is a linear example chain, not a single deep proof. It defines $\psi$, records the golden equation and $\psi \neq \varphi$, builds $L_{\mathrm{golden}}$, and tightens it against the gold phi class. A short non-forcing lemma shows $\mathrm{IsPhi}$ fails over $L_{\mathrm{golden}}$ because $\psi$ is a counter-model. Positivity selection is then defined; under it $\mathrm{IsPhi}$ becomes selected. A promotion lemma lifts that selection to a forced claim. Trivial and positive sample claims illustrate the forced-register API at the end.
why it matters in Recognition Science
T6 in the forcing chain (UnifiedForcingChain) asserts that $\varphi$ is forced by self-similarity. This module shows why a bare algebraic golden constraint is not enough: the conjugate root blocks uniqueness, so forcing fails until a positivity selection is imposed. That is the concrete lesson for the Maximal Forcing design: selection rules are first-class, and positivity is the minimal rule that recovers the RS scale.
No downstream modules are wired yet (used_by is empty); the file is an example landing pad for the phi-universe API. It still anchors the narrative that forced registers generalize from the J-cost layer to the phi layer only after selection is made explicit. Framework landmarks: T6 phi fixed point, and the broader forcing chain T0–T8.
scope and limits
- Does not prove T6 in full generality; only a concrete real-scale example.
- Does not derive positivity from deeper axioms; positivity is an input selection rule.
- Does not treat other conjugates or higher-degree self-similarity constraints.
- Does not connect to eight-tick, D=3, or constants (alpha, mass ladder).
- Does not supply downstream consumers; used_by is currently 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