`unique_on_reachN`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.LedgerUniqueness on GitHub at line 26.

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

formal source

  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

papers checked against this theorem

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