Foundation Primitive Recognition Calculus Prcinevitability Instances

The primitive distinction

The recognition calculus (a framework where events are recorded as discrete traces and each step costs something) begins with a primitive distinction: the ability to tell two things apart. The result under discussion proves that this distinction is inevitable. Any formal system that can distinguish two primitives, whether they are logical truth values, numbers, sets, or type-theoretic terms, can embed the core of the recognition calculus. The proof is not a philosophical argument but a machine-checked theorem in the framework's library of formal theorems.

The classical setting is simple. A formal system has tokens and expressions. Expressions extend one another, and a trace is a finite sequence of tokens. The first theorem states that extending a trace never shortens it: if trace T extends trace U, then the length of T is at most the length of U. This monotonicity is the backbone of the construction. It guarantees that the order of expressions by length is well-behaved, which is what allows a system to be recognized as a recognition calculus.

The key construction is ofTwoDistinct. Given any type with two distinct elements a₀ and a₁, it builds a formal system where tokens are the type's elements, expressions are natural numbers (the lengths of traces), and expression extension is the usual ≤ order on numbers. The two endpoints are a₀ and a₁. The theorem ofTwoDistinct_expressive proves that this system is expressive: it can distinguish the two endpoints. From this, the theorem two_distinct_realizes_delta shows that any such system embeds the δ core of the recognition calculus.

The result then applies this generic construction to four concrete foundations. The logical carrier distinguishes true from false. The arithmetic foundation distinguishes 0 from 1, the first distinction Peano arithmetic makes. The set-theoretic foundation distinguishes the empty set from the singleton, the 0 = ∅ versus 1 = {∅} separation that starts the von Neumann hierarchy. The type-theoretic foundation distinguishes the two closed terms of the canonical two-element type. Each of these four systems embeds the δ core, as proved by the theorems boolLogicSystem_embeds_delta, peanoSystem_embeds_delta, setFoundationSystem_embeds_delta, and typeTheorySystem_embeds_delta.

What this establishes is that the primitive distinction is not an artifact of one foundation's notation. Wherever two primitives can be told apart, the recognition calculus is already present in embryo. The final theorem, named_foundations_embed_delta, packages all four embeddings together. The reader can now see that the recognition calculus is not an exotic extra layer on top of mathematics; it is what any foundation that makes a distinction already contains.

/-- **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 (concrete).** The logical foundation contains the δ core:
distinguishing `true` from `false` is the primitive distinction, so the Law of
Logic's carrier admits a PRC embedding. -/
theorem boolLogicSystem_embeds_delta :
    Nonempty (PRCEmbeddingInto boolLogicSystem) :=
  FormalSystemEmbeddingTarget_proved boolLogicSystem boolLogicSystem_expressive

theorem peanoSystem_embeds_delta : Nonempty (PRCEmbeddingInto peanoSystem) :=
  two_distinct_realizes_delta (0 : ℕ) 1 (by decide)

theorem setFoundationSystem_embeds_delta :
    Nonempty (PRCEmbeddingInto setFoundationSystem) :=
  two_distinct_realizes_delta (∅ : Set Unit) Set.univ Set.empty_ne_univ

theorem typeTheorySystem_embeds_delta :
    Nonempty (PRCEmbeddingInto typeTheorySystem) :=
  two_distinct_realizes_delta (Sum.inl () : Unit ⊕ Unit) (Sum.inr ()) (by decide)

What this page does not claim

This module does not prove that the recognition calculus is the only possible framework, only that it is inevitable given a primitive distinction. The module does not provide a full faithful parse of any foundation, only small witnesses showing the distinction is not an artifact of Bool. The module does not derive the fine-structure constant or any physical constant; it establishes a structural fact about formal systems.

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: