IndisputableMonolith.Chain

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4
   5/-- Minimal RecognitionStructure stub for standalone compilation -/
   6structure RecognitionStructure where
   7  U : Type
   8  R : U → U → Prop
   9
  10/-- Chain structure with minimal axioms for standalone compilation -/
  11structure Chain (M : RecognitionStructure) where
  12  n : Nat
  13  f : Fin (n+1) → M.U
  14  ok : ∀ i : Fin n, M.R (f i.castSucc) (f i.succ)
  15
  16namespace Chain
  17
  18variable {M : RecognitionStructure} (ch : Chain M)
  19
  20def head : M.U := by
  21  have hpos : 0 < ch.n + 1 := Nat.succ_pos _
  22  exact ch.f ⟨0, hpos⟩
  23
  24def last : M.U := by
  25  have hlt : ch.n < ch.n + 1 := Nat.lt_succ_self _
  26  exact ch.f ⟨ch.n, hlt⟩
  27
  28end Chain
  29
  30class AtomicTick (M : RecognitionStructure) where
  31  postedAt : Nat → M.U → Prop
  32  unique_post : ∀ t : Nat, ∃! u : M.U, postedAt t u
  33
  34structure Ledger (M : RecognitionStructure) where
  35  debit : M.U → ℤ
  36  credit : M.U → ℤ
  37
  38def phi {M} (L : Ledger M) : M.U → ℤ := fun u => L.debit u - L.credit u
  39
  40def chainFlux {M} (L : Ledger M) (ch : Chain M) : ℤ :=
  41  phi L (ch.last) - phi L (ch.head)
  42
  43class Conserves {M} (L : Ledger M) : Prop where
  44  conserve : ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0
  45
  46/-- ## T2 (Atomicity): unique posting per tick implies no collision at a tick. -/
  47theorem T2_atomicity {M} [AtomicTick M] :
  48  ∀ t u v, AtomicTick.postedAt (M:=M) t u → AtomicTick.postedAt (M:=M) t v → u = v := by
  49  intro t u v hu hv
  50  rcases (AtomicTick.unique_post (M:=M) t) with ⟨w, hw, huniq⟩
  51  have hu' : u = w := huniq u hu
  52  have hv' : v = w := huniq v hv
  53  exact hu'.trans hv'.symm
  54
  55theorem T3_continuity {M} (L : Ledger M) [Conserves L] :
  56  ∀ ch : Chain M, ch.head = ch.last → chainFlux L ch = 0 := Conserves.conserve
  57
  58end IndisputableMonolith
  59