Foundation Primitive Recognition Calculus Prcdistinction Dichotomy

The distinction dichotomy

A formal system is any structure with tokens (objects) and expressions (statements about those objects). The distinction dichotomy asks a basic question about such a system: can it tell any two of its tokens apart? The answer, proved in the framework's machine-checked library of formal theorems, is that any formal system with a reflexive expression order (every expression extends itself) is either degenerate (a discrete record that distinguishes nothing, unable to tell any two objects apart) or it realizes the δ core (it can relabel its primitive endpoints onto a distinguished pair and collapse every trace to a single fixed expression).

The dichotomy is exact: degeneracy and discrimination are negations of each other. A foundation that can distinguish at least one pair of objects is discriminating, and a discriminating foundation with a reflexive expression order realizes the δ core. The only foundation that escapes δ is the one that distinguishes nothing at all, which cannot express a single non-trivial proposition. This is the δ4 headline: distinction is not optional, except for the degenerate foundation.

The hypothesis is mild. The four named foundations (logic, arithmetic, set theory, type theory) all satisfy it, and each is non-degenerate, hence realizes δ. The dichotomy is a theorem, not a conjecture: it is proved in the library with no framework-specific axioms, only the standard three axioms of the ambient type theory.

What this establishes in plain language: any foundation that can tell anything apart already contains the seed of the framework's primitive recognition calculus. The dichotomy is the first step in a chain that forces, in order, the golden ratio as the unique self-similar scaling, an eight-tick recognition cycle, 2^3, and three spatial dimensions. The distinction dichotomy is the gate: if a foundation is not degenerate, it is already on the path to the framework's structure.

/-- **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⟩)

/-- Degeneracy and discrimination are exact negations. -/
theorem not_degenerate_iff_discriminating (F : FormalSystem) :
    ¬ Degenerate F ↔ Discriminating F := by
  constructor
  · intro h
    by_contra hc
    exact h (fun a b hab => hc ⟨a, b, hab⟩)
  · rintro ⟨a, b, hab⟩ hdeg
    exact hdeg a b hab

/-- 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 four named foundations (logic, arithmetic, set theory, type theory) all
fall on the δ side of the dichotomy: each is non-degenerate, hence realizes δ. -/
theorem named_foundations_not_degenerate :
    ¬ Degenerate InevitabilityInstances.boolLogicSystem
      ∧ ¬ Degenerate InevitabilityInstances.peanoSystem
      ∧ ¬ Degenerate InevitabilityInstances.setFoundationSystem
      ∧ ¬ Degenerate InevitabilityInstances.typeTheorySystem :=
  ⟨not_degenerate_of_realizesDelta _ InevitabilityInstances.boolLogicSystem_embeds_delta,
    not_degenerate_of_realizesDelta _ InevitabilityInstances.peanoSystem_embeds_delta,
    not_degenerate_of_realizesDelta _ InevitabilityInstances.setFoundationSystem_embeds_delta,
    not_degenerate_of_realizesDelta _ InevitabilityInstances.typeTheorySystem_embeds_delta⟩

What this page does not claim

Not claiming that the δ core is the full primitive recognition calculus; it is only the seed that the dichotomy establishes. Not claiming that the four named foundations are the only non-degenerate formal systems. Not claiming that the dichotomy alone forces the golden ratio or three dimensions; it is only the first step in the chain.

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: