ClaimUniverse
plain-language theorem explainer
Packages one maximal-forcing pass as a triple: a type of realizations, an admissibility class on that type, and a set of reality claims about those realizations. Downstream forcing, independence, and classification machinery all take this package as ambient data. The declaration is a plain structure with no proof obligations.
Claim. A claim universe is a triple $(R, A, \mathcal{C})$ where $R$ is a type of realizations, $A$ is an admissibility class on $R$ (a distinguished subset of admissible realizations together with an audit label), and $\mathcal{C}$ is a set of reality claims on $R$ (each claim a labeled predicate $R \to \mathrm{Prop}$).
background
The Maximal Forcing program treats physics-facing statements as claims about realizations, then classifies each claim as forced, independent, or selected. Module setting: ForcingClosure is the claim set currently targeted by a primitive in a chosen universe; the program is complete only when every claim in that closure is so classified.
An admissibility class on a type $R$ is a pair (admissible subset of $R$, string label). The type $R$ is deliberately abstract so later phases may instantiate it with strict-logic models, costed models, or physical structures. A reality claim on $R$ is a labeled predicate holds : R → Prop; forcedness means the predicate holds on every admissible realization.
This structure is the ambient package that binds those three pieces for one forcing pass. It does not itself assert forcedness or independence; it only names the universe in which those judgments will be made.
proof idea
No proof. The declaration is a structure definition with three fields: the realization type, an admissibility class on that type, and a set of reality claims. Field types come from AdmissibilityClass and RealityClaim in the MaximalForcing stack. There are no constructors beyond the structure, no axioms, and no tactics.
why it matters
Every maximal-forcing judgment is relative to a claim universe. Downstream, ForcingClosure simply projects the claims field (execution interface for the closure operator); InClosure is membership in that set. ClaimClassification branches on forced versus independent relative to U; ForcedInvariant packages a claim that is both in-closure and forced; IndependenceWitness supplies an explicit yes/no admissible pair inside U.
Higher up, MaximalClosureCert and maximal_forcing_closure in RealityClosure certify that a whole pass has been classified. In the Recognition framework this is scaffolding for the forcing chain (T0–T8 and beyond): one fixed universe per pass, so J-uniqueness, φ, the eight-tick octave, and D = 3 can be stated as claims and then forced or witnessed independent inside a single admissible class. The open work is making the closure operator constructive from syntax/semantics rather than an opaque set field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.