Forced
plain-language theorem explainer
A reality claim is forced on an admissible class when every admissible realization satisfies it. This is the primitive universal-quantifier predicate for the Maximal Forcing program: invariants that hold on the whole admissible set. Downstream constant and dimension proofs cite it to package “no countermodel” statements. The body is a one-line definition, not a derived theorem.
Claim. Fix a type $R$ of realizations, an admissible class $A \subseteq R$, and a reality claim $C$ (a predicate $C.holds : R \to \mathrm{Prop}$ with audit label). $C$ is forced on $A$ when $\forall r_0 \in A,\; C.holds(r_0)$.
background
This module opens the Maximal Forcing Closure program: from distinction and the Law of Logic, extract every invariant true in all admissible realizations, and show every leftover degree of freedom is either forced by a deeper admissibility constraint 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-facing string label with a predicate holds on realizations. Admissible classes appear throughout the stack (recognition operators, information thermodynamics, Maxwell DEC, etc.) as the sets of realizations one is allowed to quantify over. Forcing is the universal half of that language: the claim holds on every point of the admissible set.
The sibling notion is independence: two admissible realizations disagree on the claim. Together they give the forced-versus-independent dichotomy the closure program aims at for every remaining free parameter (dimensions, ticks, constants).
proof idea
Pure definitional abbreviation. Unfolding yields the single universal statement: for every realization in the admissible set, the claim’s holds predicate is true. No lemmas, tactics, or algebraic reduction; downstream proofs simply apply or rewrite with this Prop.
why it matters
Forced is the claim-language atom for “this is not a free parameter.” Downstream uses include positivity of the fundamental tick $\tau_0$, positivity of the $\alpha^{-1}$ normalization, the configuration-space dimension identity (exactly 5), the eight-tick temporal forcing $2^D = 8$ for $D = 3$, and spatial-dimension forcing $D = 3$ (T7/T8 landmarks: eight-tick octave and three spatial dimensions). Cosmology and complex-structure modules also thread the same predicate when packaging forced combinatorial or topological facts.
In the framework, this sits under the Maximal Forcing Closure target: every invariant across admissible realizations should eventually appear as an instance of Forced, while genuine freedoms appear as Independent. The module intentionally stops short of the crown theorem; Forced only supplies the vocabulary those later closures speak.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.