T4_unique_on_component

formal source

  57  exact sub_eq_zero.mp this
  58
  59/-- Componentwise uniqueness: if p and q agree at x0, then they agree at every y reachable from x0. -/
  60theorem T4_unique_on_component {δ : ℤ} {p q : Pot M}
  61  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {x0 y : M.U}
  62  (hbase : p x0 = q x0)
  63  (hreach : Causality.Reaches (Kin M) x0 y) : p y = q y := by
  64  rcases hreach with ⟨n, h⟩
  65  exact T4_unique_on_reachN (M:=M) (δ:=δ) (p:=p) (q:=q) hp hq (x0:=x0) hbase (n:=n) (y:=y) h
  66
  67/-- If y lies in the n-ball around x0, then the two δ-potentials agree at y. -/
  68theorem T4_unique_on_inBall {δ : ℤ} {p q : Pot M}
  69  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {x0 y : M.U}
  70  (hbase : p x0 = q x0) {n : Nat}
  71  (hin : Causality.inBall (Kin M) x0 n y) : p y = q y := by
  72  rcases hin with ⟨k, _, hreach⟩
  73  exact T4_unique_on_reachN (M:=M) (δ:=δ) (p:=p) (q:=q) hp hq (x0:=x0) hbase (n:=k) (y:=y) hreach
  74
  75/-- Componentwise uniqueness up to a constant: there exists `c` (the basepoint offset)
  76    such that on the reach component of `x0` we have `p y = q y + c` for all `y`. -/
  77theorem T4_unique_up_to_const_on_component {δ : ℤ} {p q : Pot M}
  78  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {x0 : M.U} :
  79  ∃ c : ℤ, ∀ {y : M.U}, Causality.Reaches (Kin M) x0 y → p y = q y + c := by
  80  refine ⟨p x0 - q x0, ?_⟩
  81  intro y hreach
  82  have hdiff := diff_const_on_component (M:=M) (δ:=δ) (p:=p) (q:=q) hp hq (x0:=x0) (y:=y) hreach
  83  -- rearrange `p y - q y = c` to `p y = q y + c`
  84  simpa [add_comm, add_left_comm, add_assoc, sub_eq_add_neg] using
  85    (eq_add_of_sub_eq hdiff)
  86
  87/-- T8 quantization lemma: along any n-step reach, `p` changes by exactly `n·δ`. -/
  88lemma increment_on_ReachN {δ : ℤ} {p : Pot M}
  89  (hp : DE (M:=M) δ p) :
  90  ∀ {n x y}, Causality.ReachN (Kin M) n x y → p y - p x = (n : ℤ) * δ := by