increment_on_ReachN

formal source

  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
  91  intro n x y h
  92  induction h with
  93  | zero =>
  94      simp
  95  | @succ n x y z hxy hyz ih =>
  96      -- p z - p x = (p z - p y) + (p y - p x) = δ + n·δ = (n+1)·δ
  97      have hz : p z - p y = δ := hp hyz
  98      calc
  99        p z - p x = (p z - p y) + (p y - p x) := by ring
 100        _ = δ + (n : ℤ) * δ := by simpa [hz, ih]
 101        _ = ((n : ℤ) + 1) * δ := by ring
 102        _ = ((Nat.succ n : Nat) : ℤ) * δ := by
 103              simp [Nat.cast_add]
 104
 105/-- Corollary: the set of potential differences along reaches is the δ-generated subgroup. -/
 106lemma diff_in_deltaSub {δ : ℤ} {p : Pot M}
 107  (hp : DE (M:=M) δ p) {n x y}
 108  (h : Causality.ReachN (Kin M) n x y) : ∃ k : ℤ, p y - p x = k * δ := by
 109  refine ⟨(n : ℤ), ?_⟩
 110  simpa using increment_on_ReachN (M:=M) (δ:=δ) (p:=p) hp (n:=n) (x:=x) (y:=y) h
 111
 112end Potential
 113end IndisputableMonolith