IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCDistinctionDichotomy

   1/-
   2  PrimitiveRecognitionCalculus/PRCDistinctionDichotomy.lean
   3
   4  Item 4 of the δ frontier: "is distinction optional for a foundation?"
   5
   6  The prior inevitability work proved: any `Expressive` formal system (one that
   7  distinguishes the two δ endpoints) realizes the δ core, and exhibited concrete
   8  witnesses (logic, arithmetic, set theory, type theory). That answers "do these
   9  particular foundations contain δ?" but not the sharper question the δ4 lane
  10  poses: "can a foundation avoid δ at all?"
  11
  12  This module answers it as a classification theorem, not another example. For any
  13  foundation whose expression order is reflexive (every expression extends itself,
  14  which holds of any "is-derivable-from", "⊆", or "extends" relation), exactly one
  15  of two things is true:
  16
  17    * the foundation is DEGENERATE: it distinguishes no two objects whatsoever.
  18      Such a foundation cannot express the difference between a theorem and a
  19      non-theorem, between ⊤ and ⊥, between ∅ and {∅}. It cannot do mathematics.
  20
  21    * the foundation REALIZES δ: there is a PRC embedding into its own interface.
  22
  23  There is no third option, and the two are mutually exclusive. So distinction is
  24  optional ONLY for the foundation that distinguishes nothing, i.e. the one that is
  25  not a foundation for anything. Every foundation that can express a single
  26  non-trivial distinction already contains the δ core.
  27
  28  This reduces the deferred corpus task. To show a real foundation (ZFC, MLTT, a
  29  topos) contains δ, one no longer needs a bespoke δ-embedding: it suffices to
  30  exhibit ONE distinguished pair (∅ ≠ {∅}; 0 ≠ 1; ⊤ ≠ ⊥) and a reflexive
  31  derivation order, both of which any non-degenerate foundation has trivially.
  32
  33  HONEST BOUNDARY. The argument lives at the `FormalSystem` interface: `distinguishes`
  34  and `exprExtends` are the foundation's own discrimination and derivation
  35  relations. The remaining corpus task is the faithful parse that supplies those
  36  relations for a named foundation with its full expressivity. What this module
  37  removes is the need to re-prove δ-embedding for each one: the dichotomy is
  38  generic.
  39
  40  No project-local axioms. No sorry.
  41-/
  42
  43import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCInevitabilityInstances
  44
  45namespace IndisputableMonolith
  46namespace Foundation
  47namespace PrimitiveRecognitionCalculus
  48namespace DistinctionDichotomy
  49
  50open FormalSystem
  51
  52/-- A foundation distinguishes nothing: its discrimination relation is empty. It
  53cannot tell any two objects apart. -/
  54def Degenerate (F : FormalSystem) : Prop := ∀ a b : F.Token, ¬ F.distinguishes a b
  55
  56/-- A foundation discriminates if it can tell at least one pair of objects apart. -/
  57def Discriminating (F : FormalSystem) : Prop := ∃ a b : F.Token, F.distinguishes a b
  58
  59/-- A foundation's expression order is reflexive: every expression extends itself.
  60True of any "is-derivable-from" / "⊆" / "extends" relation. -/
  61def ExprReflexive (F : FormalSystem) : Prop := ∀ e : F.Expr, F.exprExtends e e
  62
  63/-- A foundation realizes the δ core: there is a PRC embedding into its own
  64interface. -/
  65def RealizesDelta (F : FormalSystem) : Prop := Nonempty (PRCEmbeddingInto F)
  66
  67/-- Degeneracy and discrimination are exact negations. -/
  68theorem not_degenerate_iff_discriminating (F : FormalSystem) :
  69    ¬ Degenerate F ↔ Discriminating F := by
  70  constructor
  71  · intro h
  72    by_contra hc
  73    exact h (fun a b hab => hc ⟨a, b, hab⟩)
  74  · rintro ⟨a, b, hab⟩ hdeg
  75    exact hdeg a b hab
  76
  77/-- A discriminating foundation with a reflexive expression order realizes the δ
  78core on its own interface: relabel the primitive endpoints onto a distinguished
  79pair, and collapse every trace to a single fixed expression. -/
  80theorem realizesDelta_of_discriminating
  81    (F : FormalSystem) (hdisc : Discriminating F) (hrefl : ExprReflexive F) :
  82    RealizesDelta F := by
  83  obtain ⟨a, b, hab⟩ := hdisc
  84  refine ⟨{
  85    endpointMap := fun e => match e.side with
  86      | Side.left => a
  87      | Side.right => b
  88    traceMap := fun _ => F.traceExpr Trace.empty
  89    preserves_distinction := ?_
  90    preserves_trace_extension := ?_ }⟩
  91  · show F.distinguishes a b
  92    exact hab
  93  · intro _ _ _
  94    exact hrefl _
  95
  96/-- Realizing δ entails discrimination: the two cases are mutually exclusive. -/
  97theorem not_degenerate_of_realizesDelta (F : FormalSystem) (h : RealizesDelta F) :
  98    ¬ Degenerate F := by
  99  obtain ⟨emb⟩ := h
 100  intro hdeg
 101  exact hdeg _ _ emb.preserves_distinction
 102
 103/-- **The dichotomy.** Any foundation with a reflexive expression order is either
 104degenerate or realizes δ. -/
 105theorem distinction_dichotomy (F : FormalSystem) (hrefl : ExprReflexive F) :
 106    Degenerate F ∨ RealizesDelta F := by
 107  by_cases h : Discriminating F
 108  · exact Or.inr (realizesDelta_of_discriminating F h hrefl)
 109  · exact Or.inl (fun a b hab => h ⟨a, b, hab⟩)
 110
 111/-- **δ4 headline: distinction is not optional, except for the degenerate
 112foundation.** For any foundation with a reflexive expression order: (i) it realizes
 113δ exactly when it can distinguish at least one pair of objects; (ii) it is either
 114degenerate or realizes δ; (iii) realizing δ rules out degeneracy. The only
 115foundation that escapes δ is the one that distinguishes nothing at all, which
 116cannot express a single non-trivial proposition. -/
 117theorem distinction_not_optional (F : FormalSystem) (hrefl : ExprReflexive F) :
 118    (RealizesDelta F ↔ Discriminating F)
 119      ∧ (Degenerate F ∨ RealizesDelta F)
 120      ∧ (RealizesDelta F → ¬ Degenerate F) := by
 121  refine ⟨⟨?_, ?_⟩, distinction_dichotomy F hrefl, not_degenerate_of_realizesDelta F⟩
 122  · intro h
 123    exact (not_degenerate_iff_discriminating F).mp (not_degenerate_of_realizesDelta F h)
 124  · intro h
 125    exact realizesDelta_of_discriminating F h hrefl
 126
 127/-! ### The hypothesis is mild: the named foundations all satisfy it -/
 128
 129theorem prcFormalSystem_exprReflexive : ExprReflexive PRCFormalSystem :=
 130  fun T => Trace.extends_refl T
 131
 132theorem ofTwoDistinct_exprReflexive {α : Type} (a₀ a₁ : α) (hne : a₀ ≠ a₁) :
 133    ExprReflexive (InevitabilityInstances.ofTwoDistinct a₀ a₁ hne) :=
 134  fun n => Nat.le_refl n
 135
 136/-- The four named foundations (logic, arithmetic, set theory, type theory) all
 137fall on the δ side of the dichotomy: each is non-degenerate, hence realizes δ. -/
 138theorem named_foundations_not_degenerate :
 139    ¬ Degenerate InevitabilityInstances.boolLogicSystem
 140      ∧ ¬ Degenerate InevitabilityInstances.peanoSystem
 141      ∧ ¬ Degenerate InevitabilityInstances.setFoundationSystem
 142      ∧ ¬ Degenerate InevitabilityInstances.typeTheorySystem :=
 143  ⟨not_degenerate_of_realizesDelta _ InevitabilityInstances.boolLogicSystem_embeds_delta,
 144    not_degenerate_of_realizesDelta _ InevitabilityInstances.peanoSystem_embeds_delta,
 145    not_degenerate_of_realizesDelta _ InevitabilityInstances.setFoundationSystem_embeds_delta,
 146    not_degenerate_of_realizesDelta _ InevitabilityInstances.typeTheorySystem_embeds_delta⟩
 147
 148end DistinctionDichotomy
 149end PrimitiveRecognitionCalculus
 150end Foundation
 151end IndisputableMonolith
 152