MaximalClosureCert
plain-language theorem explainer
A maximal closure certificate packages a total classifier: every reality claim inside the forcing closure of a primitive in a claim universe is forced, independent, or selected. Conditional crown theorems cite this interface rather than postulating completeness. It is a one-field structure; inhabiting it for a concrete universe is the actual theorem obligation.
Claim. A maximal closure certificate for a primitive $P$ and claim universe $U$ is data asserting that every reality claim $C$ in the forcing closure of $P$ relative to $U$ admits a claim classification: it is forced under $U$'s admissibility, independent (via an explicit disagreement witness), or selected (via a named selection principle).
background
This module is the crown-theorem interface for Maximal Forcing Closure. The final completeness statement is not asserted outright. Instead one records the exact certificate whose construction becomes the theorem: every claim in the forcing closure of a primitive $P$ over a claim universe $U$ is classified.
Upstream, a claim classification is an inductive Prop on a single reality claim: either the claim holds in every admissible realization (forced), or two admissible realizations disagree (independent, via an independence witness). Downstream trichotomy also surfaces a third arm, selected, which requires a named selection principle rather than a lazy contingency.
The local setting is deliberately conditional. RS-native units and related foundation machinery appear only as ambient context; the certificate itself is agnostic about which concrete universe is being classified.
proof idea
No proof body: this is a structure definition. The single field is a total map sending each reality claim in the forcing closure to a claim classification. Downstream one-line wrappers simply project that field (the conditional crown theorem is literally the certificate's classifier). Concrete inhabitations, such as the alpha-layer classifier, discharge the field by case analysis on the closed claim set.
why it matters
This is the packing type for the Maximal Forcing crown. The conditional crown theorem is the projection of the certificate's classifier; the trichotomy form rewrites that classification into the explicit disjunction Forced ∨ Independent ∨ Selected, so independence and selection remain proof obligations rather than escape hatches.
Downstream, the alpha-layer universe builds a real certificate and classifier for the fine-structure window claim. Closure-extension theorems use the certificate to show that adjoining a forced invariant preserves trichotomy and that no forced invariant can be missing: the extended universe still admits a complete classifier. The program is to inhabit this structure for the real RS claim universe, not to postulate it. That sits above the forcing chain (T5 J-uniqueness through T8 dimension) as a meta-level completeness gate on what the chain may assert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.