Foundation Maximal Forcing Primitive Primitive

The primitive starting point

In the Recognition Science framework, the declaration Primitive defines the two fundamental starting points for its Maximal Forcing program. The first, called distinction, is the bare fact that there exist two distinct things: formally, it states that there are elements x and y of a set K such that x is not equal to y. The second, called lawOfLogic, represents a realization of the framework's Law of Logic, which becomes relevant only after the initial distinction is non-vacuous. The declaration keeps these two constructors separate on purpose, so that later work can prove whether they are equivalent rather than simply assuming they are the same.

The declaration also introduces the language for talking about claims about these realizations. A RealityClaim is a structure with a human-readable label and a predicate that says whether the claim holds in a given realization. The framework then defines three possible statuses for such a claim. A claim is Forced when it holds in every admissible realization. It is Independent when two admissible realizations disagree on it, one satisfying it and the other not. Finally, a claim is Selected when it is not yet forced but has a named selection principle, an honest intermediate tag that must later be strengthened to either Forced or Independent.

This declaration deliberately does not assert the crown theorem. Its purpose is only to set up the vocabulary and the primitive starting point. The target of the broader Maximal Forcing program is to derive, from distinction and the Law of Logic, every invariant that holds across all admissible realizations, and to prove that every remaining degree of freedom is either forced by a deeper admissibility condition or shown independent by a countermodel. The Primitive declaration is the foundation stone for that program, not its conclusion.

/-- 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 declaration does not prove that any specific claim is forced or independent. It does not establish the equivalence of distinction and lawOfLogic. It does not define what makes a realization admissible.

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: