IndisputableMonolith.Foundation.MaximalForcing.AdmissibleRealization
Defines the abstract class of admissible realizations for the Maximal Forcing program. The realization type stays free so later phases can plug in strict logic models, costed models, physical models, or domain structures. Anyone tracking what counts as an admissible model under the Law of Logic would cite this layer. The module is definitional: it packages admissibility, tightening, and forced-after-tightening relations rather than proving physical identities.
claimAn admissibility class on an abstract realization type $R$ records which realizations are admissible, what counts as a tightening of a claim, and when a claim is forced after a legitimate tightening. A legitimate tightening is a refinement that strictly shrinks the admissible set while preserving already-forced claims; forcedness is monotone under such tightenings.
background
Maximal Forcing aims to derive every invariant that holds across all admissible realizations, starting from distinction and the Law of Logic (the Primitive module). Admissible realizations are the universe in which those invariants are judged: a claim is forced only if it holds in every member of that universe.
This module keeps the realization carrier $R$ deliberately abstract. Different phases may instantiate it with pure logical models, costed recognition models, physical models, or other domain structures. The local vocabulary is an admissibility class, a tightening relation on claims, forcedness after tightening, and a legitimacy predicate on tightenings (including a flip-style constructor).
Upstream, Primitive starts the claim language. Downstream, ForcingClosure treats the claim set targeted by a primitive inside a chosen universe of realizations and demands that every claim be classified as forced, independent, or selected by a named principle scheduled for further tightening.
proof idea
This is a definition module, not a theorem module. It introduces the admissibility-class structure and the associated notions of tightening, forced-after-tightening, and legitimate tightening, together with elementary lemmas such as monotonicity of forcedness under tightening and that a legitimate tightening actually reduces the admissible set. No physical forcing identity is proved here; the bodies are structural packaging for later closure arguments.
why it matters in Recognition Science
ForcingClosure imports this module as the realization universe against which a primitive's claim set is judged. Without a precise admissibility class and a notion of legitimate tightening, the closure program cannot classify claims as forced versus merely selected, nor schedule further tightenings. In the broader Recognition forcing chain, this sits under the foundation layer that eventually feeds uniqueness results (J-cost, $\varphi$, eight-tick period, $D=3$): those invariants are meaningful only once "holds in every admissible realization" is a defined predicate. The module therefore supplies the semantic side of Maximal Forcing rather than a single numbered T-step.
scope and limits
- Does not force any concrete physical constant, mass formula, or J-cost identity.
- Does not fix a concrete carrier for realizations; $R$ remains a free parameter.
- Does not classify claims as forced, independent, or selected; that is ForcingClosure's job.
- Does not prove that every legitimate tightening terminates or reaches a unique fixed point.
- Does not encode costed or physical model axioms beyond the abstract admissibility interface.