IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCInevitabilityInstances

   1/-
   2  PrimitiveRecognitionCalculus/PRCInevitabilityInstances.lean
   3
   4  Item 4 of the δ frontier: inevitability for real foundations (measured step).
   5
   6  The inevitability target is closed abstractly: any `FormalSystem` that is
   7  `Expressive` (distinguishes the two endpoints of the primitive distinction)
   8  admits a PRC embedding (`FormalSystemEmbeddingTarget_proved`). Until now the
   9  only instance was `PRCFormalSystem` (PRC modelling itself), which does not yet
  10  answer "is distinction optional for foundations built without it?".
  11
  12  This module adds the first non-self instances:
  13
  14  * `ofTwoDistinct`: a `FormalSystem` built from ANY type carrying two distinct
  15    primitives, with finite-trace length as the expression order. It is always
  16    `Expressive`, hence always embeds the δ core
  17    (`two_distinct_realizes_delta`).
  18
  19  * `boolLogicSystem`: the concrete witness. The Law of Logic's own two-valued
  20    carrier (`false ≠ true`) is a foundation that realizes δ. Distinguishing
  21    true from false IS the primitive distinction; the logical foundation
  22    therefore contains the δ core (`boolLogicSystem_embeds_delta`).
  23
  24  HONEST SCOPING (the part that stays open). This does NOT parse ZFC, dependent
  25  type theory, or elementary-topos category theory into `FormalSystem` with their
  26  full expressivity. That is the large corpus task the program defers. The exact
  27  remaining obligation, per foundation X ∈ {ZFC, MLTT/CIC, ETCS/topos}, is:
  28
  29    construct `F_X : FormalSystem` whose `Token`/`Expr` faithfully carry X's
  30    terms and derivations, exhibit two X-distinguishable primitives (e.g. ∅ vs
  31    {∅} for ZFC; 0 vs 1 in the natural-number object for a topos; the two
  32    closed terms of `Bool`/`𝟚` for MLTT), and prove `F_X.Expressive`.
  33
  34  Once `F_X.Expressive` is proved, `FormalSystemEmbeddingTarget_proved F_X`
  35  delivers the δ embedding with no further work. So the open content is purely
  36  the faithful parsing + the two-token separation for each named foundation; the
  37  inevitability step itself is already discharged. What is proved here is that
  38  the separation is the ONLY nontrivial hypothesis, and that it holds for the
  39  logical carrier.
  40
  41  No project-local axioms. No sorry.
  42-/
  43
  44import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FormalSystem
  45
  46namespace IndisputableMonolith
  47namespace Foundation
  48namespace PrimitiveRecognitionCalculus
  49namespace InevitabilityInstances
  50
  51/-- Finite-trace length is monotone under trace extension. -/
  52theorem length_le_of_extends {T U : Trace} (h : Trace.Extends T U) :
  53    Trace.length T ≤ Trace.length U := by
  54  obtain ⟨V, hV⟩ := h
  55  have key : ∀ W : Trace, Trace.length T ≤ Trace.length (Trace.append T W) := by
  56    intro W
  57    induction W with
  58    | empty => simp
  59    | extend W a ih => simpa using Nat.le_succ_of_le ih
  60  exact hV ▸ key V
  61
  62/-- A formal system built from any type with two distinct primitives. Tokens are
  63the type's elements, expressions are finite-trace lengths, and expression
  64extension is the length order. -/
  65def ofTwoDistinct {α : Type} (a₀ a₁ : α) (_hne : a₀ ≠ a₁) : FormalSystem where
  66  Token := α
  67  Expr := Nat
  68  distinguishes := fun x y => x ≠ y
  69  exprExtends := fun m n => m ≤ n
  70  endpointToken := fun e => if e.side = Side.left then a₀ else a₁
  71  traceExpr := Trace.length
  72  traceExpr_extends := fun h => length_le_of_extends h
  73
  74/-- Any system with two distinct primitives distinguishes the two endpoints. -/
  75theorem ofTwoDistinct_expressive {α : Type} (a₀ a₁ : α) (hne : a₀ ≠ a₁) :
  76    (ofTwoDistinct a₀ a₁ hne).Expressive := by
  77  unfold FormalSystem.Expressive ofTwoDistinct
  78  simp only [Endpoint.left, Endpoint.right]
  79  exact hne
  80
  81/-- **Item 4 (generic).** Any foundation exposing two distinguishable primitives
  82realizes the δ core. -/
  83theorem two_distinct_realizes_delta {α : Type} (a₀ a₁ : α) (hne : a₀ ≠ a₁) :
  84    Nonempty (PRCEmbeddingInto (ofTwoDistinct a₀ a₁ hne)) :=
  85  FormalSystemEmbeddingTarget_proved _ (ofTwoDistinct_expressive a₀ a₁ hne)
  86
  87/-- The concrete witness: the Law of Logic's own two-valued carrier. -/
  88def boolLogicSystem : FormalSystem := ofTwoDistinct false true (by decide)
  89
  90theorem boolLogicSystem_expressive : boolLogicSystem.Expressive :=
  91  ofTwoDistinct_expressive false true (by decide)
  92
  93/-- **Item 4 (concrete).** The logical foundation contains the δ core:
  94distinguishing `true` from `false` is the primitive distinction, so the Law of
  95Logic's carrier admits a PRC embedding. -/
  96theorem boolLogicSystem_embeds_delta :
  97    Nonempty (PRCEmbeddingInto boolLogicSystem) :=
  98  FormalSystemEmbeddingTarget_proved boolLogicSystem boolLogicSystem_expressive
  99
 100/-! ### Foundation-flavored witnesses
 101
 102Three further concrete instances, structurally different from the logical
 103carrier, each exhibiting the two-token separation that `ofTwoDistinct` turns into
 104a δ embedding. These are honest small witnesses, not full faithful parses of the
 105foundations (that corpus task remains, per the header), but they show the
 106distinction is not an artifact of `Bool`. -/
 107
 108/-- Arithmetic foundation: the natural-number object's `0 ≠ 1`, the first
 109distinction Peano arithmetic makes. -/
 110def peanoSystem : FormalSystem := ofTwoDistinct (0 : ℕ) 1 (by decide)
 111
 112theorem peanoSystem_embeds_delta : Nonempty (PRCEmbeddingInto peanoSystem) :=
 113  two_distinct_realizes_delta (0 : ℕ) 1 (by decide)
 114
 115/-- Set-theoretic foundation: the empty set differs from the singleton (here
 116`∅ ≠ univ` on a one-point domain), the `0 = ∅` vs `1 = {∅}` separation that starts
 117the von Neumann hierarchy. -/
 118def setFoundationSystem : FormalSystem :=
 119  ofTwoDistinct (∅ : Set Unit) Set.univ Set.empty_ne_univ
 120
 121theorem setFoundationSystem_embeds_delta :
 122    Nonempty (PRCEmbeddingInto setFoundationSystem) :=
 123  two_distinct_realizes_delta (∅ : Set Unit) Set.univ Set.empty_ne_univ
 124
 125/-- Type-theoretic foundation: the canonical two-element type `𝟚 = Unit ⊕ Unit`,
 126whose two closed terms are distinct. -/
 127def typeTheorySystem : FormalSystem :=
 128  ofTwoDistinct (Sum.inl () : Unit ⊕ Unit) (Sum.inr ()) (by decide)
 129
 130theorem typeTheorySystem_embeds_delta :
 131    Nonempty (PRCEmbeddingInto typeTheorySystem) :=
 132  two_distinct_realizes_delta (Sum.inl () : Unit ⊕ Unit) (Sum.inr ()) (by decide)
 133
 134/-- **Item 4, widened.** Four structurally different foundations, the logical
 135two-valued carrier, the arithmetic `0 ≠ 1`, the set-theoretic `∅ ≠ {∅}`, and the
 136type-theoretic `𝟚`, each realize the δ core. The primitive distinction is not an
 137artifact of one foundation's notation; it appears wherever two primitives can be
 138told apart. -/
 139theorem named_foundations_embed_delta :
 140    Nonempty (PRCEmbeddingInto boolLogicSystem)
 141      ∧ Nonempty (PRCEmbeddingInto peanoSystem)
 142      ∧ Nonempty (PRCEmbeddingInto setFoundationSystem)
 143      ∧ Nonempty (PRCEmbeddingInto typeTheorySystem) :=
 144  ⟨boolLogicSystem_embeds_delta, peanoSystem_embeds_delta,
 145    setFoundationSystem_embeds_delta, typeTheorySystem_embeds_delta⟩
 146
 147end InevitabilityInstances
 148end PrimitiveRecognitionCalculus
 149end Foundation
 150end IndisputableMonolith
 151