SelectionPrinciple
plain-language theorem explainer
Names a provisional selection rule for a reality claim that is not yet forced on a given admissible class of realizations. Audit and closure work cite it when tagging intermediate status before Forced or Independent is proved. The declaration is a two-field structure (audit label plus applicability proposition), not a theorem.
Claim. For a type $R$ of realizations, an admissible class $A \subseteq R$, and a reality claim $C$ (a predicate on $R$ with audit metadata), a selection principle is a named pair consisting of a string label and a proposition asserting that the principle applies. It records a provisional rule used when $C$ is not forced on $A$.
background
This module opens the Maximal Forcing Closure program: from distinction and the Law of Logic, derive every invariant shared by all admissible realizations, and classify every leftover degree of freedom as forced by a deeper admissibility condition or independent by countermodel. The file only fixes the primitive claim language; it does not assert the crown theorem.
A reality claim is a labeled predicate holds on realizations. Forced means the claim holds on every member of the admissible class. Independent means two admissible realizations disagree on it. Selection principles sit between those poles: named reasons to prefer one side when the claim is not yet forced on the current class.
The admissible class and claim are parameters; the structure itself carries only audit-facing metadata and an applicability proposition, so later work can strengthen the status to Forced or Independent without rewriting the claim language.
proof idea
No proof. This is a structure definition with two fields: an audit string label and a proposition applies. Instantiation is by providing those fields (as in the positivity example that sets the label to the expanding-root rule and applies to $\varphi > 0$).
why it matters
Selection principles are the honest middle tag in the forcing trichotomy. Downstream, Selected is defined as "not Forced on the admissible class, yet inhabited by some SelectionPrinciple." That tag is explicitly provisional: it must later be strengthened to Forced or Independent.
The first concrete use is positivitySelection in the RS selection example: positivity picks the expanding root for the golden scale-ratio claim over the golden-only admissible class, so "$r = \varphi$" is Selected rather than Forced. That is the third branch of the local trichotomy and keeps the Maximal Forcing ledger auditable while deeper admissibility (T5–T8 style forcing of $J$, $\varphi$, the eight-tick octave, $D = 3$) is still being closed.
Without this structure, intermediate preferences would be smuggled in as Forced or left unlabeled; with it, every non-forced choice is named and must eventually be discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.