IndisputableMonolith.Recognition

   1import Mathlib
   2-- LightCone is not required by the minimal Recognition core; avoid heavy deps
   3
   4namespace IndisputableMonolith
   5namespace Recognition
   6
   7/-! ### T1 (MP): Nothing cannot recognize itself -/
   8
   9abbrev Nothing := Empty
  10
  11/-- Minimal recognizer→recognized pairing. -/
  12structure Recognize (A : Type) (B : Type) : Type where
  13  recognizer : A
  14  recognized : B
  15
  16/-- MP: It is impossible for Nothing to recognize itself. -/
  17def MP : Prop := ¬ ∃ _ : Recognize Nothing Nothing, True
  18
  19theorem mp_holds : MP := by
  20  intro h
  21  rcases h with ⟨⟨r, _⟩, _⟩
  22  cases r
  23
  24/-- Alias used in the manuscript: "Nonexistence cannot recognize itself." -/
  25abbrev NothingCannotRecognizeItself : Prop := MP
  26
  27/-- Direct alias proof of MP for the manuscript phrasing. -/
  28theorem nothing_cannot_recognize_itself : NothingCannotRecognizeItself :=
  29  mp_holds
  30
  31structure RecognitionStructure where
  32  U : Type
  33  R : U → U → Prop
  34
  35structure Chain (M : RecognitionStructure) where
  36  n : Nat
  37  f : Fin (n+1) → M.U
  38  ok : ∀ i : Fin n, M.R (f i.castSucc) (f i.succ)
  39
  40namespace Chain
  41variable {M : RecognitionStructure} (ch : Chain M)
  42def head : M.U := by
  43  have hpos : 0 < ch.n + 1 := Nat.succ_pos _
  44  exact ch.f ⟨0, hpos⟩
  45def last : M.U := by
  46  have hlt : ch.n < ch.n + 1 := Nat.lt_succ_self _
  47  exact ch.f ⟨ch.n, hlt⟩
  48end Chain
  49
  50structure Ledger (M : RecognitionStructure) where
  51  debit : M.U → ℤ
  52  credit : M.U → ℤ
  53
  54@[simp] def Ledger.Carrier {M : RecognitionStructure} (_ : Ledger M) : Type :=
  55  M.U
  56
  57def phi {M} (L : Ledger M) : M.U → ℤ := fun u => L.debit u - L.credit u
  58
  59def chainFlux {M} (L : Ledger M) (ch : Chain M) : ℤ :=
  60  phi L (Chain.last ch) - phi L (Chain.head ch)
  61
  62class Conserves {M} (L : Ledger M) : Prop where
  63  conserve : ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0
  64
  65lemma chainFlux_zero_of_loop {M} (L : Ledger M) [Conserves L] (ch : Chain M) (h : ch.head = ch.last) :
  66  chainFlux L ch = 0 := Conserves.conserve (L:=L) ch h
  67
  68lemma phi_zero_of_balanced {M} (L : Ledger M) (hbal : ∀ u, L.debit u = L.credit u) :
  69  ∀ u, phi L u = 0 := by
  70  intro u; simp [phi, hbal u, sub_self]
  71
  72lemma chainFlux_zero_of_balanced {M} (L : Ledger M) (ch : Chain M)
  73  (hbal : ∀ u, L.debit u = L.credit u) :
  74  chainFlux L ch = 0 := by
  75  simp [chainFlux, phi_zero_of_balanced (M:=M) L hbal]
  76
  77class AtomicTick (M : RecognitionStructure) where
  78  postedAt : Nat → M.U → Prop
  79  unique_post : ∀ t : Nat, ∃! u : M.U, postedAt t u
  80
  81theorem T2_atomicity {M} [AtomicTick M] :
  82  ∀ t u v, AtomicTick.postedAt (M:=M) t u → AtomicTick.postedAt (M:=M) t v → u = v := by
  83  intro t u v hu hv
  84  rcases (AtomicTick.unique_post (M:=M) t) with ⟨w, hw, huniq⟩
  85  have huw : u = w := huniq u hu
  86  have hvw : v = w := huniq v hv
  87  exact huw.trans hvw.symm
  88
  89end Recognition
  90
  91namespace Demo
  92
  93open Recognition
  94
  95structure U where
  96  a : Unit
  97
  98/-- Recognition relation by structural equality -/
  99def recog : U → U → Prop := fun x y => x = y
 100
 101def M : RecognitionStructure := { U := U, R := recog }
 102
 103def L : Ledger M := { debit := fun _ => 1, credit := fun _ => 1 }
 104
 105def twoStep : Chain M :=
 106  { n := 1
 107  , f := fun _ => ⟨()⟩
 108  , ok := by intro i; trivial }
 109
 110example : chainFlux L twoStep = 0 := by
 111  have hbal : ∀ u, L.debit u = L.credit u := by intro _; rfl
 112  simpa [chainFlux_zero_of_balanced (M:=M) L twoStep hbal]
 113
 114end Demo
 115
 116-- Moved advanced Recognition sections (ClassicalBridge, Potential uniqueness) to Recognition/WIP.lean during modularization.
 117