Pith. sign in
module module moderate

IndisputableMonolith.Foundation.MaximalForcing.RealityClosure

show as:
view Lean formalization →

Defines the maximal closure certificate that packages a complete forced/independent/selected classification over a primitive and claim universe. Downstream RS universe modules (cost, phi, alpha, gravity, hbar, mass ladder) import it as the shared scaffold for single-constant forcing. The argument is structural: a certificate plus a trichotomy lemma that every claim lands in exactly one class.

claimA maximal closure certificate for a primitive set $P$ and claim universe $U$ is a complete classification of every claim in $U$ as forced, independent, or selected relative to an admissibility class on realizations of $P$. The module also records the trichotomy that these three classes partition $U$, and a session-update protocol for revising the certificate when the claim set grows.

background

Maximal forcing is the RS program that turns "what must be true of any admissible recognition cost / coupling / ladder" into a machine-checked classification. Upstream, ForcedInvariant states the rule: every claim in a closure target must eventually be tagged Forced, Independent, or Selected. Selected is an honest temporary tag, not an endpoint; it must be promoted by a deeper admissibility condition or demoted by countermodel.

This module sits one layer above that classification language. It introduces the certificate object that says a given claim universe is fully classified, together with the structural lemmas that make "complete classifier" a usable hypothesis in later single-constant universes. The local setting is foundation-level: no physics constants yet, only the abstract carrier of primitives, claims, and admissibility.

Sibling names in the module (certificate, closure theorem, trichotomy, session-update protocol) are the reusable API that Phase-1/Phase-2 universe files import rather than re-proving classification hygiene each time.

proof idea

Definition-and-certificate module, not a deep analytic proof. It packages: (1) the maximal-closure certificate type bundling a complete classifier over a claim universe; (2) a closure theorem asserting that certificate implies every claim is forced, independent, or selected; (3) a trichotomy lemma that the three classes are exhaustive and disjoint; (4) a session-update protocol describing how the certificate may be extended when new claims are added. Concrete forcing work is deferred to the importing universe modules, which supply admissibility and discharge Selected tags.

why it matters in Recognition Science

This is the shared scaffold for the entire MaximalForcing stack. RSCostUniverse roots Phase 1 in the published J-cost uniqueness theorem; RSPhiUniverse, RSAlphaUniverse, RSGravityUniverse, RSHbarUniverse, and RSMassLadderUniverse are the Phase-2 single-constant instantiations (phi fixed point, alpha construction window, Einstein coupling $8\varphi^5$, action quantum $\varphi^{-5}$, phi-ladder mass scaling). RSClosureExtension uses the same certificate language to prove stability under extension by a forced invariant.

Without a uniform closure certificate, each physics-adjacent layer would reinvent completeness and trichotomy. The module therefore earns its place as the framework-level answer to "when is a claim universe closed under maximal forcing," feeding every downstream RS*Universe import and the carrier-extension stability result. It does not itself force T5–T8 or the RCL; those enter only when a concrete universe plugs in the corresponding admissibility gates.

scope and limits

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)