Foundation Maximal Forcing Reality Closure Maximal Closure Cert

The closure certificate

Recognition Science (a framework that derives physical structure from a ledger, a discrete record of recognition events) defines a formal goal: for any starting primitive and any universe of claims, every claim that lies in the forcing closure must receive one of three verdicts. The declaration MaximalClosureCert states the exact shape of the certificate that would achieve this. It is a structure, not a proof: it asserts that a classifier exists which, for every claim in the closure, returns a classification of Forced, Independent, or Selected.

The three verdicts carry distinct meanings. A Forced claim is one the framework's axioms entail. An Independent claim comes with an explicit countermodel witness, a concrete structure showing the claim does not follow. A Selected claim rests on a named selection principle, a deliberate choice rather than a consequence. The trichotomy theorem in the same module shows that, given such a certificate, every claim in the closure indeed falls into exactly one of these three categories. This is the literal "as forced as possible" statement: it concedes no contingency lazily, because even Independence and Selection are proof obligations, not defaults.

The declaration is deliberately conditional. The docstring states plainly that the final theorem is not asserted here; instead, the module states the certificate whose construction will be the theorem. The program is to build MaximalClosureCert for the real universe, not to postulate it. A separate session protocol tracks progress toward that goal, recording whether a session landed a new forced invariant, added an independence witness, tightened admissibility, or updated the execution plan with the exact remaining blocker.

What this does not claim is as important as what it asserts. The existence of MaximalClosureCert for the actual physical universe is not proved; it remains a target. The certificate itself is not a claim about physics directly, but about a formal classification of claims. And the trichotomy does not say every claim is decidable in practice, only that each falls into one of three categories given the certificate. The declaration is a scaffold for a future proof, not the proof itself.

/-- A maximal closure certificate for a primitive and claim universe. -/
structure MaximalClosureCert (P : Primitive) (U : ClaimUniverse.{u}) where
  classifies :
    forall C : RealityClaim U.Realization,
      InClosure P U C -> ClaimClassification U C

/-- Crown theorem in the exact disjunction form: given a classifier certificate,
every claim in the forcing closure is `Forced`, `Independent`, or `Selected`.
This is the literal "as forced as possible" statement; it concedes no contingency
lazily, because `Independent` and `Selected` are themselves proof obligations
(an explicit countermodel witness and a named selection principle, respectively).
-/
theorem maximal_forcing_closure_trichotomy
    {P : Primitive} {U : ClaimUniverse.{u}} (cert : MaximalClosureCert P U)
    (C : RealityClaim U.Realization) (hC : InClosure P U C) :
    Forced U.admissibility.admissible C ∨
    Independent U.admissibility.admissible C ∨
    Selected U.admissibility.admissible C := by
  rcases cert.classifies C hC with h | hw | hs
  · exact Or.inl h
  · exact Or.inr (Or.inl (independent_of_witness hw))
  · exact Or.inr (Or.inr hs)

/-- A maximal closure certificate for a primitive and claim universe. -/
structure MaximalClosureCert (P : Primitive) (U : ClaimUniverse.{u}) where
  classifies :
    forall C : RealityClaim U.Realization,
      InClosure P U C -> ClaimClassification U C

What this page does not claim

The certificate for the actual physical universe exists; it is a target, not a result. Every claim in the closure is forced; some may be independent or selected. The trichotomy guarantees practical decidability of all claims.

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/RealityClosure.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: