Foundation Maximal Forcing Rsclosure Extension Mem Extend Of Mem

Closure under extension

Recognition Science keeps a ledger, a discrete record of claims about reality, each one tagged as forced, independent, or selected. A forced claim is one the framework's own laws compel; an independent claim is one that needs an explicit countermodel to be classified; a selected claim rests on a named choice principle. The theorem mem_extend_of_mem addresses a simple worry: if the ledger already classifies every claim in its universe, what happens when someone adds a new claim to the list?

The answer, proved in the framework's machine-checked library of formal theorems, is that nothing breaks. The theorem states that any claim already in the closure of the original ledger remains in the closure after the ledger is extended with a new claim. The extension changes only the set of claims, leaving the realization type and admissibility class untouched, so every prior classification survives verbatim. The new claim, if it is forced, lands in the forced bucket; if it is independent or selected, it slots in with its own certificate. The register is saturated under classified extension: no forced invariant can ever be missing in a way that breaks the closure.

What this does not claim is broader than what it does. The theorem does not say that every physically real invariant has already been discovered, nor that the ledger is complete in an absolute sense. It says only that the framework's classification machinery is stable under extension: if a new claim is proposed, the only work is producing its classification certificate, not repairing the ledger's structure. Undiscovered independence or selection remains possible; undiscovered forced invariants are absorbed automatically. The structural guarantee is about closure, not omniscience.

/-- Old claims remain in the extended closure. -/
theorem mem_extend_of_mem {P : Primitive} {U : ClaimUniverse.{u}}
    {C0 C : RealityClaim U.Realization} (h : InClosure P U C) :
    InClosure P (U.extend C0) C :=
  Set.mem_insert_of_mem _ h

/-- **THE REGISTER IS SATURATED UNDER CLASSIFIED EXTENSION (THEOREM).** This is the
complete structural statement of carrier-completeness, covering all three buckets at
once. A complete classifier survives adjoining any claim `C₀` for which a
classification certificate (`ClaimClassification U C₀`) exists. Equivalently: the
predicate "this universe has a complete classifier" is closed under extension by any
classifiable claim.

The honest reading: the curated carrier cannot be "incomplete" in any way the framework
fails to absorb. If a new physically-real invariant is proposed, exactly one of three
things happens, and all three are handled — it is `Forced` (absorbed automatically, the
yard/eos-style derivations), `Independent` (absorbed once you exhibit a countermodel),
or `Selected` (absorbed once you name a selection principle). The residual content of
the maximal-forcing program is never "find the missing slot in the register"; it is
always "produce the classification certificate for a specific proposed claim." -/
theorem register_saturated_under_classification {P : Primitive} {U : ClaimUniverse.{u}}
    (cert : MaximalClosureCert P U) {C0 : RealityClaim U.Realization}
    (h0 : ClaimClassification U C0) :
    Nonempty (MaximalClosureCert P (U.extend C0)) :=
  ⟨cert.extendClassified h0⟩

@[simp] theorem extend_realization (U : ClaimUniverse.{u}) (C0 : RealityClaim U.Realization) :
    (U.extend C0).Realization = U.Realization := rfl

@[simp] theorem extend_admissibility (U : ClaimUniverse.{u}) (C0 : RealityClaim U.Realization) :
    (U.extend C0).admissibility = U.admissibility := rfl

What this page does not claim

The ledger contains every physically real invariant that will ever be discovered. The framework can classify any claim without producing a certificate. The theorem applies to claims outside the ledger's realization type and admissibility class.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/MaximalForcing/RSClosureExtension.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: