edge_diff_invariant

formal source

  18def Kin (M : Recognition.RecognitionStructure) : Causality.Kinematics M.U := { step := M.R }
  19
  20/-- On each edge, the difference (p − q) is invariant if both satisfy the same δ rule. -/
  21lemma edge_diff_invariant {δ : ℤ} {p q : Pot M}
  22  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {a b : M.U} (h : M.R a b) :
  23  (p b - q b) = (p a - q a) := by
  24  have harr : (p b - q b) - (p a - q a) = (p b - p a) - (q b - q a) := by ring
  25  have hδ : (p b - p a) - (q b - q a) = δ - δ := by simp [hp h, hq h]
  26  have : (p b - q b) - (p a - q a) = 0 := by simp [harr, hδ]
  27  exact sub_eq_zero.mp this
  28
  29/-- The difference (p − q) is constant along any n‑step reach. -/
  30lemma diff_const_on_ReachN {δ : ℤ} {p q : Pot M}
  31  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) :
  32  ∀ {n x y}, Causality.ReachN (Kin M) n x y → (p y - q y) = (p x - q x) := by
  33  intro n x y h
  34  induction h with
  35  | zero => rfl
  36  | @succ n x y z hxy hyz ih =>
  37      have h_edge : (p z - q z) = (p y - q y) :=
  38        edge_diff_invariant (M:=M) (δ:=δ) (p:=p) (q:=q) hp hq hyz
  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}