IndisputableMonolith.Foundation.MaximalForcing.Primitive

   1import Mathlib
   2
   3/-!
   4# Maximal Forcing: Primitive and Claim Language
   5
   6This module starts the Maximal Forcing Closure program.
   7
   8The target is:
   9
  10* from distinction / Law of Logic, derive every invariant that is invariant
  11  across all admissible realizations;
  12* prove every remaining degree of freedom is either forced by a deeper
  13  admissibility condition or independent by countermodel.
  14
  15This file only defines the primitive and claim language. It intentionally does
  16not assert the crown theorem.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace MaximalForcing
  22
  23universe u
  24
  25/-- The primitive starting point for maximal forcing. The two constructors are
  26kept distinct so later modules can prove their equivalence rather than silently
  27identify them. -/
  28inductive Primitive where
  29  /-- Object-level distinction: `exists x y : K, x != y`. -/
  30  | distinction
  31  /-- Law-of-Logic realization, after the floor is non-vacuous. -/
  32  | lawOfLogic
  33  deriving DecidableEq, Repr
  34
  35/-- A claim about realizations. The `label` is audit-facing metadata; the theorem
  36content is the predicate `holds`. -/
  37structure RealityClaim (R : Type u) where
  38  label : String
  39  holds : R -> Prop
  40
  41/-- A claim is forced on an admissible class when it holds in every admissible
  42realization. -/
  43def Forced {R : Type u} (Admissible : Set R) (C : RealityClaim R) : Prop :=
  44  ∀ R0 : R, R0 ∈ Admissible -> C.holds R0
  45
  46/-- A claim is independent over an admissible class when two admissible
  47realizations disagree on it. -/
  48def Independent {R : Type u} (Admissible : Set R) (C : RealityClaim R) : Prop :=
  49  ∃ R0 R1 : R,
  50    R0 ∈ Admissible ∧ R1 ∈ Admissible ∧ C.holds R0 ∧ ¬ C.holds R1
  51
  52/-- A named selection principle for claims not yet forced on the current
  53admissible class. -/
  54structure SelectionPrinciple {R : Type u} (Admissible : Set R)
  55    (C : RealityClaim R) where
  56  label : String
  57  applies : Prop
  58
  59/-- A claim is selected when it is not forced on the current admissible class but
  60does have a named selection principle. This is not final closure; it is an
  61honest tag that must later be strengthened to `Forced` or `Independent`. -/
  62def Selected {R : Type u} (Admissible : Set R) (C : RealityClaim R) : Prop :=
  63  ¬ Forced Admissible C ∧ Nonempty (SelectionPrinciple Admissible C)
  64
  65end MaximalForcing
  66end Foundation
  67end IndisputableMonolith
  68