Pith. sign in
module module moderate

IndisputableMonolith.Foundation.MaximalForcing.ForcedInvariant

show as:
view Lean formalization →

Defines how a single claim is classified inside one maximal-forcing closure universe: forced invariant versus independent. Downstream RealityClosure imports this as the certificate atom. The module is definitional scaffolding for the crown certificate, not a proved uniqueness theorem.

claimIn a fixed closure universe $U$ for a forcing program $P$, each claim $C$ receives a classification: either $C$ is a forced invariant of every maximal closure of $P$ in $U$, or else an independence witness (countermodel pair) is required. The module packages that classification type and the forced-invariant predicate.

background

Maximal Forcing treats physical and logical structure as what every admissible closure of a forcing program must share. Upstream IndependenceWitness states the dual: if a claim is not forced, maximal closure demands an explicit countermodel pair rather than a vague appeal to contingency.

This module sits between that witness language and the RealityClosure certificate. It introduces the local vocabulary for one claim in one universe: a classification object that records whether the claim is invariant under all closures, and the forced-invariant side of that dichotomy.

The setting is Foundation-level, prior to concrete RS landmarks (J-cost uniqueness, $\varphi$, eight-tick period, $D=3$). Those enter only when the certificate is instantiated on the actual forcing chain.

proof idea

This is a definition module, not a proof module. It declares the classification type for one claim in one closure universe and the forced-invariant predicate used by that classification. No forcing uniqueness or completeness argument is carried here; those belong to RealityClosure and the theorems that build its certificate.

why it matters in Recognition Science

RealityClosure is the crown-theorem interface for Maximal Forcing Closure. Its doc-comment states the exact certificate shape: for every claim $C$ in a forcing closure of $P$ in $U$, one must supply a ClaimClassification of $C$ in $U$. This module supplies that classification atom and the ForcedInvariant side of the split.

Without a sharp forced-versus-independent dichotomy, the crown certificate cannot be stated. The module therefore earns its place as the typed hinge between IndependenceWitness (what non-forced claims must exhibit) and RealityClosure (the forall-claims certificate). It does not itself close the RS forcing chain T0–T8; it only names the invariant status those chain steps must eventually receive.

scope and limits

used by (1)

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 (2)