`ReachN`

definition

show as: view math explainer →

module: IndisputableMonolith.LedgerUniqueness
domain: LedgerUniqueness
line: 9 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.LedgerUniqueness on GitHub at line 9.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

   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')

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.