ClaimClassification
plain-language theorem explainer
Every reality claim in a maximal-forcing universe is tagged as forced (true in all admissible realizations), independent (split by an explicit countermodel pair), or selected (held by a named selection principle, not yet forced). Closure certificates and crown theorems cite this trichotomy as the target type of a complete classifier. It is an inductive Prop with three constructors, each carrying its witness.
Claim. Fix a claim universe $U$ (realizations, an admissibility class, and a set of claims) and a reality claim $C$ on $U$'s realizations. Then $C$ is classified by exactly one of: (i) forcedness of $C$ over the admissible class; (ii) an independence witness (two admissible models that disagree on $C$); (iii) a selection certificate that $C$ is governed by a named selection principle without yet being forced.
background
Maximal forcing asks that every claim in a closure target eventually land in one of three buckets: forced, independent, or selected. The module states that Selected is an honest temporary tag, not an endpoint: it must be promoted to forced by a deeper admissibility condition or demoted to independent by countermodel.
A claim universe packages a type of realizations, an admissibility class on that type, and a set of reality claims. Forcedness means the claim holds on every admissible realization. An independence witness is an explicit pair of admissible models, one satisfying the claim and one failing it. Selection is the residual bucket for claims pinned by a named principle short of full forcedness.
Upstream, the independence-witness structure supplies the countermodel pair (yes-model, no-model, both admissible, disagreeing on the claim). The forcing-closure layer supplies the claim-universe carrier that this classification is indexed by.
proof idea
No proof body: this is an inductive proposition with three constructors. Each constructor is a thin wrapper around an existing witness type. The forced constructor takes a proof that the claim is forced over the universe's admissible class. The independent constructor takes an independence witness (two admissible realizations that disagree). The selected constructor takes a selection certificate relative to the same admissible class. Classification is therefore just the disjoint union of those three witness types, as a Prop.
why it matters
This trichotomy is the codomain of every complete classifier in the maximal-forcing stack. A maximal closure certificate is exactly a map sending every claim in the forcing closure to a classification. The conditional crown theorem maximal_forcing_closure is the one-line projection of that certificate: once a classifier exists, every closed claim is forced, independent, or selected.
Downstream, the alpha-layer universe builds an explicit classifier into this type. Carrier-completeness theorems use it as the extension key: adjoining any claim that already carries a classification preserves existence of a complete classifier, and forced invariants remain forced after extension. In the Recognition forcing program this is the bookkeeping layer that turns the T0–T8 uniqueness chain into a closed register of claims rather than an open list of open questions. Selected remains the only temporary bucket; the program is to empty it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.