Selected
plain-language theorem explainer
A reality claim is selected on an admissible class when it is not forced there, yet a named selection principle for it exists. Closure and classification theorems cite this status as the third arm of the forced/independent/selected trichotomy. The body is a pure conjunction: negation of universal holding plus nonempty selection-principle data. It is an honest interim tag, meant to be promoted later to forced or independent.
Claim. A claim $C$ about realizations of type $R$ is selected relative to an admissible class $A \subseteq R$ when $C$ is not forced on $A$ (it is not the case that every $r \in A$ satisfies $C$) and there exists a named selection principle for $C$ over $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 prove every leftover degree of freedom is either 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 packages an audit label with a predicate holds on realizations. Forced means the predicate holds on every member of the admissible class. Independent means two admissible realizations disagree on it. A selection principle is a named structure (label plus an applicability proposition) attached to a claim that is not yet forced.
Admissibility itself is imported as a set of realizations (in MaxwellDEC media, strictly positive material parameters). Selected sits between forced and independent: not universally true on the current class, but already equipped with an explicit selection rule rather than left unclassified.
proof idea
Pure definitional abbreviation, not a proved theorem. The proposition is the conjunction of (i) negation of Forced on the given admissible set and claim, and (ii) Nonempty of the SelectionPrinciple structure for that pair. No lemmas are applied; unfolding yields exactly those two conjuncts.
why it matters
Selected is the third disjunct in the crown trichotomy. The conditional crown theorem maximal_forcing_closure and its disjunctive form maximal_forcing_closure_trichotomy assert that every claim in the forcing closure is Forced, Independent, or Selected, once a MaximalClosureCert exists. Downstream ClaimClassification inductives and RSClosureExtension results (extend_preserves_trichotomy, forced_invariant_absorbed, MaximalClosureCert) thread this status through universe extension.
Tightening structures mark the intended promotion path: a claim forced after a stricter admissibility class is a target to move from Selected to Forced. In the broader Recognition forcing chain (T0–T8), this tag keeps residual degrees of freedom honest until they are absorbed by deeper admissibility or discharged by countermodel, rather than smuggling contingency into the closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.