IndisputableMonolith.Potential

   1import Mathlib
   2import IndisputableMonolith.Recognition
   3import IndisputableMonolith.Causality.Basic
   4
   5namespace IndisputableMonolith
   6namespace Potential
   7
   8/-! Dependency-light T4 uniqueness lemmas on discrete reach sets. -/
   9
  10variable {M : Recognition.RecognitionStructure}
  11
  12abbrev Pot (M : Recognition.RecognitionStructure) := M.U → ℤ
  13
  14/-- Discrete edge rule: along any edge, `p` increases by `δ` on `M.R`. -/
  15def DE (δ : ℤ) (p : Pot M) : Prop := ∀ {a b}, M.R a b → p b - p a = δ
  16
  17/-- Package the recognition relation as a kinematics. -/
  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}
  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⟩
  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
  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
 114