Foundation Primitive Recognition Calculus Prctype Theory Parse No Confusion

The two-token distinction

In ordinary logic, a two-valued system has exactly two truth values, usually called false and true. The declaration no_confusion states that these two values are distinct: false is not true, and true is not false. This is not a subtle philosophical point; it is the bare minimum for any system that wants to tell two things apart. Without this distinction, the words “false” and “true” would be interchangeable, and every statement about them would collapse into a single blob. The declaration is a theorem in the framework’s machine-checked library of formal theorems, proved by a direct case analysis on the two values.

The framework models a primitive recognition event, a single act of telling one thing from another, as a choice between two tokens. In this model, the two tokens are exactly the two truth values. The declaration no_confusion is what guarantees that the two tokens are genuinely different, so that a recognition event can actually distinguish one alternative from the other. Along with a companion theorem stating that every closed term of the two-valued type is either false or true, this gives the type its full character: exactly two inhabitants, and they are not the same. The framework then packages these two facts together as a single theorem that its foundational system realizes a minimal core of distinction.

What no_confusion does not claim is just as important. It does not say anything about which of the two values is “better” or “preferred”; it only says they are different. It does not assert that the two values exhaust all possibilities by themselves; that is the separate canonicity theorem. And it does not claim that the framework’s own recognition events are the only way to model distinction; it only shows that this particular two-valued type, the one from Martin-Löf type theory, satisfies the required property. The declaration is a local fact about a two-element type, not a global statement about the nature of reality.

For the reader, the practical consequence is simple: when the framework speaks of a recognition event, it is speaking about a real distinction, not a mere label swap. The two tokens are fixed and separate, and any reasoning built on top of them can rely on that separation. This is the foundation on which the framework’s later claims about cost and structure are built.

/-- **No-confusion / constructor disjointness.** The two canonical terms are
distinct: this is the recursor's verdict, the type theory's own distinction. -/
theorem no_confusion : (false : Two) ≠ true := by decide

/-- **The faithful parse, packaged.** Type theory's two-element type satisfies
canonicity (exactly two closed terms) and no-confusion (they are distinct), and the
foundation realizes the δ core. -/
theorem type_theory_realizes_delta :
    (∀ b : Two, b = false ∨ b = true)
      ∧ ((false : Two) ≠ true)
      ∧ Nonempty (PRCEmbeddingInto ttSystem) :=
  ⟨canonicity, no_confusion, ttSystem_embeds_delta⟩

What this page does not claim

No_confusion alone does not prove that the two values exhaust all possibilities; that is the separate canonicity theorem. The declaration does not assert any preference or ordering between false and true. The framework does not claim that its two-token model is the only way to represent distinction in type theory.

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