Foundation Maximal Forcing Primitive

The starting vocabulary

Maximal forcing is a research program within Recognition Science that asks a sharp question: once you assume reality keeps a discrete record of events, which features of that record are unavoidable, and which could be different? The program's name comes from its ambition. It wants to force, or derive, every invariant that holds across all admissible realizations, and to prove that every remaining degree of freedom is either pinned down by a deeper condition or genuinely independent. This primitive is the vocabulary that makes the question possible to state at all.

The primitive defines two starting points. The first is distinction: the bare fact that a universe contains at least two different things, written formally as the existence of two distinct elements. The second is law of logic: a realization that respects the rules of logic itself, after the floor of distinction is non-vacuous. These two constructors are deliberately kept separate. The design choice is that later work should prove their equivalence rather than silently identify them, so the framework can audit exactly what each assumption contributes.

On top of these primitives, the framework defines the language of claims. A reality claim is a predicate on a realization, tagged with a label for auditing. A claim is forced on an admissible class when it holds in every admissible realization. A claim is independent when two admissible realizations disagree on it, one satisfying it and one not. A third status, selected, marks a claim that is not yet forced but has a named selection principle; this is an honest intermediate tag that must later be strengthened to forced or independent.

The primitive intentionally stops short of asserting any crown theorem. It establishes only the language in which the maximal forcing program will be conducted. The payoff of this restraint is precision: every future claim in the program can be classified as forced, independent, or selected, and the classification itself is machine-checked. What a reader can now see is the exact skeleton of an argument that aims to show which features of a discrete reality are logically unavoidable and which are free choices.

/-- The primitive starting point for maximal forcing. The two constructors are
kept distinct so later modules can prove their equivalence rather than silently
identify them. -/
inductive Primitive where
  /-- Object-level distinction: `exists x y : K, x != y`. -/
  | distinction
  /-- Law-of-Logic realization, after the floor is non-vacuous. -/
  | lawOfLogic
  deriving DecidableEq, Repr

/-- A claim is forced on an admissible class when it holds in every admissible
realization. -/
def Forced {R : Type u} (Admissible : Set R) (C : RealityClaim R) : Prop :=
  ∀ R0 : R, R0 ∈ Admissible -> C.holds R0

/-- A claim is independent over an admissible class when two admissible
realizations disagree on it. -/
def Independent {R : Type u} (Admissible : Set R) (C : RealityClaim R) : Prop :=
  ∃ R0 R1 : R,
    R0 ∈ Admissible ∧ R1 ∈ Admissible ∧ C.holds R0 ∧ ¬ C.holds R1

/-- A claim is selected when it is not forced on the current admissible class but
does have a named selection principle. This is not final closure; it is an
honest tag that must later be strengthened to `Forced` or `Independent`. -/
def Selected {R : Type u} (Admissible : Set R) (C : RealityClaim R) : Prop :=
  ¬ Forced Admissible C ∧ Nonempty (SelectionPrinciple Admissible C)

What this page does not claim

This primitive does not assert that any particular claim is forced or independent. This primitive does not prove the crown theorem of maximal forcing. This primitive does not define what counts as an admissible realization.

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