Foundation Primitive Recognition Calculus Prcdistinction Dichotomy Realizes Delt

The distinction dichotomy

A formal system is a set of tokens and rules for deriving expressions from them. The Recognition Science framework asks when such a system can express a basic kind of distinction: the ability to tell one token from another. The declaration realizesDelta_of_discriminating proves that any formal system which can distinguish at least one pair of tokens, and whose expression relation is reflexive (every expression extends itself), can embed the primitive recognition calculus into its own interface. In plain terms: if a system can tell anything apart at all, it already has the structure needed to recognize a fundamental distinction.

The theorem is part of a dichotomy. A degenerate foundation, one whose discrimination relation is empty, cannot tell any two objects apart. The framework proves that any foundation with a reflexive expression order is either degenerate or realizes the delta core, and that realizing delta rules out degeneracy. The only way to escape the delta core is to be a system that distinguishes nothing, which cannot express a single non-trivial proposition. This means distinction is not optional for any useful foundation: logic, arithmetic, set theory, and type theory all fall on the delta side of the dichotomy.

What the theorem does not claim is just as important. It does not say that every discriminating system is identical to the primitive recognition calculus. It says only that such a system can embed the delta core, meaning it can relabel the primitive endpoints onto a distinguished pair and collapse traces to a fixed expression. The theorem also does not assert that any particular physical system realizes delta; it is a statement about formal systems and their expressive power, not about the physical world. The physical recognition-to-linking bridge remains open.

/-- A discriminating foundation with a reflexive expression order realizes the δ
core on its own interface: relabel the primitive endpoints onto a distinguished
pair, and collapse every trace to a single fixed expression. -/
theorem realizesDelta_of_discriminating
    (F : FormalSystem) (hdisc : Discriminating F) (hrefl : ExprReflexive F) :
    RealizesDelta F := by
  obtain ⟨a, b, hab⟩ := hdisc
  refine ⟨{
    endpointMap := fun e => match e.side with
      | Side.left => a
      | Side.right => b
    traceMap := fun _ => F.traceExpr Trace.empty
    preserves_distinction := ?_
    preserves_trace_extension := ?_ }⟩
  · show F.distinguishes a b
    exact hab
  · intro _ _ _
    exact hrefl _

/-- **The dichotomy.** Any foundation with a reflexive expression order is either
degenerate or realizes δ. -/
theorem distinction_dichotomy (F : FormalSystem) (hrefl : ExprReflexive F) :
    Degenerate F ∨ RealizesDelta F := by
  by_cases h : Discriminating F
  · exact Or.inr (realizesDelta_of_discriminating F h hrefl)
  · exact Or.inl (fun a b hab => h ⟨a, b, hab⟩)

/-- Realizing δ entails discrimination: the two cases are mutually exclusive. -/
theorem not_degenerate_of_realizesDelta (F : FormalSystem) (h : RealizesDelta F) :
    ¬ Degenerate F := by
  obtain ⟨emb⟩ := h
  intro hdeg
  exact hdeg _ _ emb.preserves_distinction

What this page does not claim

The theorem does not claim that every discriminating system is identical to the primitive recognition calculus, only that it can embed the delta core. The theorem does not assert that any particular physical system realizes delta. The theorem does not establish the physical recognition-to-linking bridge, which remains open.

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