IndisputableMonolith.LedgerUniqueness

   1import Mathlib
   2import IndisputableMonolith.Recognition
   3import IndisputableMonolith.Potential
   4import IndisputableMonolith.Causality.Basic
   5-- For standalone WIP, inline a minimal Kinematics to avoid module dependency
   6namespace Local
   7structure Kinematics (α : Type) where
   8  step : α → α → Prop
   9inductive ReachN {α} (K : Kinematics α) : Nat → α → α → Prop
  10| zero {x} : ReachN K 0 x x
  11| succ {n x y z} : ReachN K n x y → K.step y z → ReachN K (n+1) x z
  12def inBall {α} (K : Kinematics α) (x : α) (n : Nat) (y : α) : Prop := ∃ k ≤ n, ReachN K k x y
  13def Reaches {α} (K : Kinematics α) (x y : α) : Prop := ∃ n, ReachN K n x y
  14end Local
  15
  16namespace IndisputableMonolith
  17namespace LedgerUniqueness
  18
  19open Recognition
  20
  21variable {M : Recognition.RecognitionStructure}
  22
  23def IsAffine (δ : ℤ) (L : Recognition.Ledger M) : Prop :=
  24  Potential.DE (M:=M) δ (fun x => Recognition.phi L x)
  25
  26lemma unique_on_reachN {δ : ℤ} {L L' : Recognition.Ledger M}
  27  (hL : IsAffine (M:=M) δ L) (hL' : IsAffine (M:=M) δ L')
  28  {x0 : M.U} (hbase : Recognition.phi L x0 = Recognition.phi L' x0) :
  29  ∀ {n y}, Causality.ReachN (Potential.Kin M) n x0 y →
  30    Recognition.phi L y = Recognition.phi L' y := by
  31  intro n y hreach
  32  have : (fun x => Recognition.phi L x) y = (fun x => Recognition.phi L' x) y := by
  33    refine Potential.T4_unique_on_reachN (M:=M) (δ:=δ)
  34      (p:=fun x => Recognition.phi L x) (q:=fun x => Recognition.phi L' x)
  35      hL hL' (x0:=x0) (by simpa using hbase) (n:=n) (y:=y) hreach
  36  simpa using this
  37
  38lemma unique_on_inBall {δ : ℤ} {L L' : Recognition.Ledger M}
  39  (hL : IsAffine (M:=M) δ L) (hL' : IsAffine (M:=M) δ L')
  40  {x0 y : M.U} (hbase : Recognition.phi L x0 = Recognition.phi L' x0) {n : Nat}
  41  (hin : Causality.inBall (Potential.Kin M) x0 n y) :
  42  Recognition.phi L y = Recognition.phi L' y := by
  43  exact Potential.T4_unique_on_inBall (M:=M) (δ:=δ)
  44    (p:=fun x => Recognition.phi L x) (q:=fun x => Recognition.phi L' x)
  45    hL hL' (x0:=x0) (by simpa using hbase) (n:=n) hin
  46
  47lemma unique_up_to_const_on_component {δ : ℤ} {L L' : Recognition.Ledger M}
  48  (hL : IsAffine (M:=M) δ L) (hL' : IsAffine (M:=M) δ L')
  49  {x0 : M.U} : ∃ c : ℤ, ∀ {y : M.U}, Causality.Reaches (Potential.Kin M) x0 y →
  50    Recognition.phi L y = Recognition.phi L' y + c := by
  51  simpa using
  52    (Potential.T4_unique_up_to_const_on_component (M:=M) (δ:=δ)
  53      (p:=fun x => Recognition.phi L x) (q:=fun x => Recognition.phi L' x)
  54      hL hL' (x0:=x0))
  55
  56end LedgerUniqueness
  57end IndisputableMonolith
  58
  59
  60