diff_const_on_component

formal source

  39      exact h_edge.trans ih
  40
  41/-- On reach components, the difference (p − q) equals its basepoint value. -/
  42lemma diff_const_on_component {δ : ℤ} {p q : Pot M}
  43  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {x0 y : M.U}
  44  (hreach : Causality.Reaches (Kin M) x0 y) :
  45  (p y - q y) = (p x0 - q x0) := by
  46  rcases hreach with ⟨n, h⟩
  47  simpa using diff_const_on_ReachN (M:=M) (δ:=δ) (p:=p) (q:=q) hp hq (n:=n) (x:=x0) (y:=y) h
  48
  49/-- If two δ‑potentials agree at a basepoint, they agree on its n-step reach set. -/
  50theorem T4_unique_on_reachN {δ : ℤ} {p q : Pot M}
  51  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {x0 : M.U}
  52  (hbase : p x0 = q x0) : ∀ {n y}, Causality.ReachN (Kin M) n x0 y → p y = q y := by
  53  intro n y h
  54  have hdiff := diff_const_on_ReachN (M:=M) (δ:=δ) (p:=p) (q:=q) hp hq h
  55  have : p x0 - q x0 = 0 := by simp [hbase]
  56  have : p y - q y = 0 := by simpa [this] using hdiff
  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⟩