Foundation Primitive Recognition Calculus Prcinevitability Instances Two Distinc

The primitive distinction

The declaration two_distinct_realizes_delta is a theorem in the framework's machine-checked library of formal theorems. It states that any formal system with at least two distinguishable primitives can realize the core of the primitive recognition calculus, a structure the framework calls the delta core. The proof is constructive: given any two distinct objects, the theorem builds a formal system whose tokens are those objects, whose expressions are natural numbers, and whose notion of expression extension is the usual ordering on numbers. The two objects serve as the system's two endpoints, and the theorem shows this system is expressive, meaning it can tell those endpoints apart.

The framework's recognition calculus, the discrete record of events and their costs, requires a primitive distinction to get started. This theorem shows that distinction is unavoidable: wherever two things can be told apart, the delta core already exists. The library then applies the theorem to four concrete foundations. The logical carrier distinguishes true from false. Peano arithmetic distinguishes 0 from 1. Set theory distinguishes the empty set from its singleton. Type theory distinguishes the two canonical terms of the two-element type. Each of these four systems embeds the delta core, and a single named theorem packages all four embeddings together.

What the theorem does not claim is just as important. It does not claim that any of these four systems is a complete or faithful model of the full recognition calculus. The library's own documentation calls these "honest small witnesses" and notes that the task of parsing entire foundations remains open. The theorem establishes only that the delta core, the minimal two-endpoint structure, appears in each system. It says nothing about whether the richer structures of the recognition calculus, such as the cost function or the eight-tick cycle, are forced in any of these foundations. Those claims, if they exist, live in other theorems.

/-- **Item 4 (generic).** Any foundation exposing two distinguishable primitives
realizes the δ core. -/
theorem two_distinct_realizes_delta {α : Type} (a₀ a₁ : α) (hne : a₀ ≠ a₁) :
    Nonempty (PRCEmbeddingInto (ofTwoDistinct a₀ a₁ hne)) :=
  FormalSystemEmbeddingTarget_proved _ (ofTwoDistinct_expressive a₀ a₁ hne)

/-- **Item 4 (generic).** Any foundation exposing two distinguishable primitives
realizes the δ core. -/
theorem two_distinct_realizes_delta {α : Type} (a₀ a₁ : α) (hne : a₀ ≠ a₁) :
    Nonempty (PRCEmbeddingInto (ofTwoDistinct a₀ a₁ hne)) :=
  FormalSystemEmbeddingTarget_proved _ (ofTwoDistinct_expressive a₀ a₁ hne)

/-- **Item 4, widened.** Four structurally different foundations, the logical
two-valued carrier, the arithmetic `0 ≠ 1`, the set-theoretic `∅ ≠ {∅}`, and the
type-theoretic `𝟚`, each realize the δ core. The primitive distinction is not an
artifact of one foundation's notation; it appears wherever two primitives can be
told apart. -/
theorem named_foundations_embed_delta :
    Nonempty (PRCEmbeddingInto boolLogicSystem)
      ∧ Nonempty (PRCEmbeddingInto peanoSystem)
      ∧ Nonempty (PRCEmbeddingInto setFoundationSystem)
      ∧ Nonempty (PRCEmbeddingInto typeTheorySystem) :=
  ⟨boolLogicSystem_embeds_delta, peanoSystem_embeds_delta,
    setFoundationSystem_embeds_delta, typeTheorySystem_embeds_delta⟩

/-- **Item 4, widened.** Four structurally different foundations, the logical
two-valued carrier, the arithmetic `0 ≠ 1`, the set-theoretic `∅ ≠ {∅}`, and the
type-theoretic `𝟚`, each realize the δ core. The primitive distinction is not an
artifact of one foundation's notation; it appears wherever two primitives can be
told apart. -/
theorem named_foundations_embed_delta :
    Nonempty (PRCEmbeddingInto boolLogicSystem)
      ∧ Nonempty (PRCEmbeddingInto peanoSystem)
      ∧ Nonempty (PRCEmbeddingInto setFoundationSystem)
      ∧ Nonempty (PRCEmbeddingInto typeTheorySystem) :=
  ⟨boolLogicSystem_embeds_delta, peanoSystem_embeds_delta,
    setFoundationSystem_embeds_delta, typeTheorySystem_embeds_delta⟩

What this page does not claim

The theorem does not prove that Peano arithmetic or set theory is a complete model of the recognition calculus. The theorem does not derive the cost function J from the existence of two distinct primitives. The theorem does not claim that the delta core is the only structure common to all four foundations.

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/PrimitiveRecognitionCalculus/PRCInevitabilityInstances.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: