RealityClaim
plain-language theorem explainer
A reality claim is a named predicate on a type of realizations: audit label plus a proposition-valued map. It is the atomic unit of the Maximal Forcing Closure language. Anyone classifying forced versus independent invariants cites it. The declaration is a bare structure with no proof obligations.
Claim. Fix a type $R$ of realizations. A reality claim on $R$ is a pair $(\ell, P)$ where $\ell$ is a string label and $P : R \to \mathrm{Prop}$ is the mathematical content: the claim holds at $r$ precisely when $P(r)$ is true.
background
The Maximal Forcing Closure program aims to derive every invariant that is stable across all admissible realizations, starting from distinction and the Law of Logic, and to show that every leftover degree of freedom is either forced by a deeper admissibility condition or independent by countermodel. This module only installs the primitive and claim language; it does not assert the crown theorem.
A reality claim is the carrier for that language. The label is audit-facing metadata. The theorem content is the predicate holds, which asks whether a given realization satisfies the claim. Downstream, a claim is called forced on an admissible class when it holds in every admissible realization, and independent when two admissible realizations disagree on it.
Related admissibility filters appear elsewhere in the stack (recognition operator, information thermodynamics, neutrino baseline search), but this structure is deliberately parametric in the realization type $R$ and does not hard-wire any particular admissibility predicate.
proof idea
No proof. The declaration is a two-field structure: a String label and a predicate R → Prop. Instantiation is by supplying both fields; there are no axioms, constructors beyond the structure, or tactic steps.
why it matters
Every forced-invariant and independence argument in Maximal Forcing is typed over this carrier. Downstream, Forced and Independent quantify over holds; ForcedAfterTightening packages a claim forced on a narrowed admissibility class as a promotion target from Selected to Forced; forced_of_forced_under_tightening shows forcedness is preserved under tightening; tightening_does_work extracts an excluded realization from an independence-to-forcing flip; ClaimClassification is the forced-versus-independent dichotomy on a claim universe; ForcedInvariant pairs a claim in the closure with a forcedness proof; ClaimUniverse and ForcingClosure assemble the full claim set.
In framework terms this is the bookkeeping layer under the forcing chain (T0–T8): once J-uniqueness, φ, the eight-tick octave, and D = 3 are in place, residual degrees of freedom are stated as reality claims and classified. The module intentionally stops short of the crown theorem; this structure is the vocabulary that theorem will speak.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.