IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic

   1/-
   2  PrimitiveRecognitionCalculus/Basic.lean
   3
   4  Round-trip source:
   5    PRC_Kernel_Spec_20260526.html
   6
   7  Spec anchors:
   8    K2.1-K2.5, R1-R4
   9
  10  The δ-only syntactic kernel: distinction act, side, endpoint, finite
  11  trace, trace append, and trace extension. Lean equality is used only by
  12  the verifier to prove facts about this syntax.
  13-/
  14
  15import Mathlib
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Strength
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace PrimitiveRecognitionCalculus
  21
  22/-- K2.1. The primitive distinction act. At the object level this is δ. -/
  23inductive DistinctionAct where
  24  | delta
  25  deriving DecidableEq, Repr
  26
  27/-- K2.2. The two sides forced by a distinction. -/
  28inductive Side where
  29  | left
  30  | right
  31  deriving DecidableEq, Repr
  32
  33/-- K2.3. An endpoint is a side of the primitive distinction. -/
  34structure Endpoint where
  35  side : Side
  36  deriving DecidableEq, Repr
  37
  38/-- The left endpoint of δ. -/
  39def Endpoint.left : Endpoint :=
  40  ⟨Side.left⟩
  41
  42/-- The right endpoint of δ. -/
  43def Endpoint.right : Endpoint :=
  44  ⟨Side.right⟩
  45
  46/-- K2.4. A finite trace is empty or extended by one distinction act. -/
  47inductive Trace where
  48  | empty
  49  | extend : Trace → DistinctionAct → Trace
  50  deriving DecidableEq, Repr
  51
  52namespace Trace
  53
  54/-- R3. One-step extension by δ. -/
  55def step (T : Trace) : Trace :=
  56  Trace.extend T DistinctionAct.delta
  57
  58/-- Append two traces. This is the syntactic composition operation. -/
  59def append : Trace → Trace → Trace
  60  | T, Trace.empty => T
  61  | T, Trace.extend U a => Trace.extend (append T U) a
  62
  63@[simp] theorem append_empty (T : Trace) :
  64    append T Trace.empty = T := by
  65  rfl
  66
  67@[simp] theorem append_extend (T U : Trace) (a : DistinctionAct) :
  68    append T (Trace.extend U a) = Trace.extend (append T U) a := by
  69  rfl
  70
  71@[simp] theorem empty_append (T : Trace) :
  72    append Trace.empty T = T := by
  73  induction T with
  74  | empty => rfl
  75  | extend T a ih =>
  76      simp [append, ih]
  77
  78/-- R4. Trace append is associative. -/
  79theorem append_assoc (T U V : Trace) :
  80    append (append T U) V = append T (append U V) := by
  81  induction V with
  82  | empty => rfl
  83  | extend V a ih =>
  84      simp [append, ih]
  85
  86/-- K2.5. `Extends T U` means `U` is `T` followed by some suffix trace. -/
  87def Extends (T U : Trace) : Prop :=
  88  ∃ V : Trace, append T V = U
  89
  90/-- R4. Trace extension is reflexive. -/
  91theorem extends_refl (T : Trace) :
  92    Extends T T := by
  93  exact ⟨Trace.empty, rfl⟩
  94
  95/-- R4. Trace extension is transitive. -/
  96theorem extends_trans {T U V : Trace}
  97    (hTU : Extends T U) (hUV : Extends U V) :
  98    Extends T V := by
  99  rcases hTU with ⟨A, hA⟩
 100  rcases hUV with ⟨B, hB⟩
 101  refine ⟨append A B, ?_⟩
 102  rw [← append_assoc, hA, hB]
 103
 104/-- The trace with exactly `n` repeated δ-extensions. -/
 105def orbitTrace : Nat → Trace
 106  | 0 => Trace.empty
 107  | Nat.succ n => step (orbitTrace n)
 108
 109/-- Length of a finite trace. -/
 110def length : Trace → Nat
 111  | Trace.empty => 0
 112  | Trace.extend T _ => Nat.succ (length T)
 113
 114@[simp] theorem length_empty :
 115    length Trace.empty = 0 := by
 116  rfl
 117
 118@[simp] theorem length_extend (T : Trace) (a : DistinctionAct) :
 119    length (Trace.extend T a) = Nat.succ (length T) := by
 120  rfl
 121
 122/-- K2.12 preview. The length of the nth orbit trace is n. -/
 123theorem length_orbitTrace (n : Nat) :
 124    length (orbitTrace n) = n := by
 125  induction n with
 126  | zero => rfl
 127  | succ n ih =>
 128      simp [orbitTrace, step, ih]
 129
 130end Trace
 131
 132end PrimitiveRecognitionCalculus
 133end Foundation
 134end IndisputableMonolith
 135