Pith. sign in
module module moderate

IndisputableMonolith.Foundation.MaximalForcing.RSClosureExtension

show as:
view Lean formalization →

Extension layer for the Maximal Forcing reality-closure certificate: it lifts a realization, its admissibility data, and its claim set into a larger closed universe while preserving trichotomy and absorbing forced invariants. Anyone building or auditing the crown certificate (every claim in the forcing closure is classified) cites these lemmas. The module is mostly membership and preservation lemmas over the RealityClosure interface.

claimGiven a forcing universe $U$ and a realization of a closed claim set, form an extended realization and extended claim set so that: the original claims remain members; the new claim sits in the extended closure; trichotomy of claim classification is preserved; forced invariants are absorbed; and a saturated register remains saturated under classification.

background

Maximal Forcing aims at a single crown certificate: for every claim $C$ in the forcing closure of a package $P$ relative to a universe $U$, the claim is classified (proved, conditional, definitional, or scaffolding). The upstream module RealityClosure states that certificate as an interface and does not yet assert the final theorem.

This module sits one layer out. It treats an already-admissible realization and produces an extended realization and extended claim family. Sibling names indicate the usual closure operations: membership of the self-extension and of prior members, preservation of the three-way classification split, absorption of forced invariants into the closed set, and a saturation register under classification.

Notation follows the Foundation forcing chain: claims live in a forcing closure, admissibility packages the structural hypotheses needed for classification, and extension is the monotone step that adds a new claim without breaking prior certificates.

proof idea

Definition-and-lemma module, not a single crown proof. It introduces extend operations on realizations, admissibility bundles, and claim sets, then proves the expected membership facts (self-membership; old members remain members). Preservation lemmas show trichotomy of classification survives extension and that forced invariants are absorbed. A final register lemma records that a saturated classification state remains saturated after the extension step. Arguments are the standard monotone-closure pattern over the RealityClosure interface rather than deep analytic estimates.

why it matters in Recognition Science

Without a controlled extension step, the crown certificate in RealityClosure cannot grow when a new RS claim is forced. This module supplies that step inside Maximal Forcing: it keeps the closed universe coherent while new claims (including RS-native ones) are registered and classified. Downstream use is the assembly of the full forcing-closure certificate (every $C$ in the closure is classified). In the broader Recognition framework it supports the T0–T8 forcing chain by ensuring each newly forced landmark can be absorbed without breaking prior classification or admissibility.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)