Reaches

formal source

  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) (δ:=δ)