IndisputableMonolith.Foundation.SimplicialLedger.DirichletAction

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Algebra.BigOperators.Fin
   3import Mathlib.Tactic.Linarith
   4import Mathlib.Tactic.Ring
   5
   6/-!
   7# Finite weighted-graph Dirichlet action
   8
   9This module isolates the finite weighted-graph action used by the simplicial
  10ledger continuum bridge. Its imports are Mathlib-only. The action, Laplacian,
  11and pairing identities below contain no physical normalization or continuum
  12endpoint assumptions.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Foundation
  17namespace SimplicialLedger
  18namespace ContinuumBridge
  19
  20noncomputable section
  21
  22/-! ## Definitions -/
  23
  24/-- A weighted simplicial graph representing the ledger. -/
  25structure WeightedLedgerGraph (n : ℕ) where
  26  weight : Fin n → Fin n → ℝ
  27  weight_nonneg : ∀ i j, 0 ≤ weight i j
  28  weight_symm : ∀ i j, weight i j = weight j i
  29
  30/-- The discrete Laplacian action (= quadratic J-cost) on the graph. -/
  31def laplacian_action {n : ℕ} (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) : ℝ :=
  32  (1 / 2) * ∑ i : Fin n, ∑ j : Fin n, G.weight i j * (ε i - ε j) ^ 2
  33
  34/-- The discrete Laplacian of ε at vertex i:
  35    (Δε)_i = Σ_j w_ij · (ε_i − ε_j) -/
  36def discrete_laplacian {n : ℕ} (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) (i : Fin n) : ℝ :=
  37  ∑ j : Fin n, G.weight i j * (ε i - ε j)
  38
  39/-- The finite pairing `⟨η, Δε⟩`. -/
  40def laplacian_pairing {n : ℕ} (G : WeightedLedgerGraph n)
  41    (η ε : Fin n → ℝ) : ℝ :=
  42  ∑ i : Fin n, η i * discrete_laplacian G ε i
  43
  44/-- The symmetric polar form of the discrete Laplacian action. -/
  45def laplacian_bilinear {n : ℕ} (G : WeightedLedgerGraph n)
  46    (ε η : Fin n → ℝ) : ℝ :=
  47  (1 / 2) * ∑ i : Fin n, ∑ j : Fin n,
  48    G.weight i j * (ε i - ε j) * (η i - η j)
  49
  50/-! ## Finite-sum algebra -/
  51
  52private theorem right_weighted_sum_eq_neg_left {n : ℕ}
  53    (G : WeightedLedgerGraph n) (ε η : Fin n → ℝ) :
  54    (∑ i : Fin n, ∑ j : Fin n,
  55        G.weight i j * (ε i - ε j) * η j)
  56      =
  57    -∑ i : Fin n, ∑ j : Fin n,
  58        G.weight i j * (ε i - ε j) * η i := by
  59  calc
  60    (∑ i : Fin n, ∑ j : Fin n,
  61        G.weight i j * (ε i - ε j) * η j)
  62        =
  63      ∑ j : Fin n, ∑ i : Fin n,
  64        G.weight i j * (ε i - ε j) * η j := by
  65          rw [Finset.sum_comm]
  66    _ =
  67      ∑ i : Fin n, ∑ j : Fin n,
  68        G.weight j i * (ε j - ε i) * η i := by
  69          rfl
  70    _ =
  71      ∑ i : Fin n, ∑ j : Fin n,
  72        G.weight i j * (ε j - ε i) * η i := by
  73          refine Finset.sum_congr rfl (fun i _ => ?_)
  74          refine Finset.sum_congr rfl (fun j _ => ?_)
  75          rw [G.weight_symm]
  76    _ =
  77      -∑ i : Fin n, ∑ j : Fin n,
  78        G.weight i j * (ε i - ε j) * η i := by
  79          rw [← Finset.sum_neg_distrib]
  80          refine Finset.sum_congr rfl (fun i _ => ?_)
  81          rw [← Finset.sum_neg_distrib]
  82          refine Finset.sum_congr rfl (fun j _ => ?_)
  83          ring
  84
  85private theorem pairing_eq_left_weighted_sum {n : ℕ}
  86    (G : WeightedLedgerGraph n) (ε η : Fin n → ℝ) :
  87    laplacian_pairing G η ε
  88      =
  89    ∑ i : Fin n, ∑ j : Fin n,
  90      G.weight i j * (ε i - ε j) * η i := by
  91  unfold laplacian_pairing discrete_laplacian
  92  calc
  93    (∑ i : Fin n, η i * ∑ j : Fin n,
  94        G.weight i j * (ε i - ε j))
  95        =
  96      ∑ i : Fin n, ∑ j : Fin n,
  97        η i * (G.weight i j * (ε i - ε j)) := by
  98          refine Finset.sum_congr rfl (fun i _ => ?_)
  99          rw [Finset.mul_sum]
 100    _ =
 101      ∑ i : Fin n, ∑ j : Fin n,
 102        G.weight i j * (ε i - ε j) * η i := by
 103          refine Finset.sum_congr rfl (fun i _ => ?_)
 104          refine Finset.sum_congr rfl (fun j _ => ?_)
 105          ring
 106
 107/-! ## Exact Dirichlet identities -/
 108
 109/-- The edge polar form is exactly the Laplacian pairing `⟨η, Δε⟩`. -/
 110theorem laplacian_bilinear_eq_pairing {n : ℕ}
 111    (G : WeightedLedgerGraph n) (ε η : Fin n → ℝ) :
 112    laplacian_bilinear G ε η = laplacian_pairing G η ε := by
 113  unfold laplacian_bilinear
 114  let L : ℝ :=
 115    ∑ i : Fin n, ∑ j : Fin n,
 116      G.weight i j * (ε i - ε j) * η i
 117  let R : ℝ :=
 118    ∑ i : Fin n, ∑ j : Fin n,
 119      G.weight i j * (ε i - ε j) * η j
 120  have hR : R = -L := by
 121    dsimp [R, L]
 122    exact right_weighted_sum_eq_neg_left G ε η
 123  have hdiff :
 124      (∑ i : Fin n, ∑ j : Fin n,
 125        G.weight i j * (ε i - ε j) * (η i - η j)) = 2 * L := by
 126    calc
 127      (∑ i : Fin n, ∑ j : Fin n,
 128        G.weight i j * (ε i - ε j) * (η i - η j))
 129          = L - R := by
 130              dsimp [L, R]
 131              rw [← Finset.sum_sub_distrib]
 132              refine Finset.sum_congr rfl (fun i _ => ?_)
 133              rw [← Finset.sum_sub_distrib]
 134              refine Finset.sum_congr rfl (fun j _ => ?_)
 135              ring
 136      _ = 2 * L := by
 137            rw [hR]
 138            ring
 139  calc
 140    (1 / 2) * ∑ i : Fin n, ∑ j : Fin n,
 141        G.weight i j * (ε i - ε j) * (η i - η j)
 142        = L := by
 143            rw [hdiff]
 144            ring
 145    _ = laplacian_pairing G η ε := by
 146          exact (pairing_eq_left_weighted_sum G ε η).symm
 147
 148/-- The polar form is symmetric in its two fields. -/
 149theorem laplacian_bilinear_comm {n : ℕ}
 150    (G : WeightedLedgerGraph n) (ε η : Fin n → ℝ) :
 151    laplacian_bilinear G ε η = laplacian_bilinear G η ε := by
 152  unfold laplacian_bilinear
 153  congr 1
 154  refine Finset.sum_congr rfl (fun i _ => ?_)
 155  refine Finset.sum_congr rfl (fun j _ => ?_)
 156  ring
 157
 158/-- The discrete Laplacian is self-adjoint for the finite pairing. -/
 159theorem laplacian_pairing_comm {n : ℕ}
 160    (G : WeightedLedgerGraph n) (ε η : Fin n → ℝ) :
 161    laplacian_pairing G η ε = laplacian_pairing G ε η := by
 162  rw [← laplacian_bilinear_eq_pairing G ε η,
 163    laplacian_bilinear_comm,
 164    laplacian_bilinear_eq_pairing]
 165
 166/-- The Dirichlet energy is exactly the Laplacian quadratic pairing. -/
 167theorem laplacian_action_eq_pairing {n : ℕ}
 168    (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) :
 169    laplacian_action G ε = laplacian_pairing G ε ε := by
 170  calc
 171    laplacian_action G ε = laplacian_bilinear G ε ε := by
 172      unfold laplacian_action laplacian_bilinear
 173      congr 1
 174      refine Finset.sum_congr rfl (fun i _ => ?_)
 175      refine Finset.sum_congr rfl (fun j _ => ?_)
 176      ring
 177    _ = laplacian_pairing G ε ε :=
 178      laplacian_bilinear_eq_pairing G ε ε
 179
 180private theorem double_sum_mul_left {n : ℕ}
 181    (c : ℝ) (f : Fin n → Fin n → ℝ) :
 182    (∑ i : Fin n, ∑ j : Fin n, c * f i j)
 183      = c * ∑ i : Fin n, ∑ j : Fin n, f i j := by
 184  calc
 185    (∑ i : Fin n, ∑ j : Fin n, c * f i j)
 186        = ∑ i : Fin n, c * ∑ j : Fin n, f i j := by
 187            refine Finset.sum_congr rfl (fun i _ => ?_)
 188            rw [Finset.mul_sum]
 189    _ = c * ∑ i : Fin n, ∑ j : Fin n, f i j := by
 190          rw [Finset.mul_sum]
 191
 192/-- Exact polynomial expansion of the action along the line `ε + tη`.
 193The linear coefficient is forced to be `2 * ⟨η, Δε⟩` by the action's
 194ordered-edge normalization. -/
 195theorem laplacian_action_line_expansion {n : ℕ}
 196    (G : WeightedLedgerGraph n) (ε η : Fin n → ℝ) (t : ℝ) :
 197    laplacian_action G (fun i => ε i + t * η i)
 198      =
 199    laplacian_action G ε
 200      + 2 * t * laplacian_pairing G η ε
 201      + t ^ 2 * laplacian_action G η := by
 202  have hsum :
 203      (∑ i : Fin n, ∑ j : Fin n,
 204        G.weight i j *
 205          ((ε i + t * η i) - (ε j + t * η j)) ^ 2)
 206        =
 207      (∑ i : Fin n, ∑ j : Fin n,
 208        G.weight i j * (ε i - ε j) ^ 2)
 209        + 2 * t * (∑ i : Fin n, ∑ j : Fin n,
 210          G.weight i j * (ε i - ε j) * (η i - η j))
 211        + t ^ 2 * (∑ i : Fin n, ∑ j : Fin n,
 212          G.weight i j * (η i - η j) ^ 2) := by
 213    calc
 214      (∑ i : Fin n, ∑ j : Fin n,
 215        G.weight i j *
 216          ((ε i + t * η i) - (ε j + t * η j)) ^ 2)
 217          =
 218        ∑ i : Fin n, ∑ j : Fin n,
 219          (G.weight i j * (ε i - ε j) ^ 2
 220            + (2 * t) *
 221                (G.weight i j * (ε i - ε j) * (η i - η j))
 222            + t ^ 2 * (G.weight i j * (η i - η j) ^ 2)) := by
 223              refine Finset.sum_congr rfl (fun i _ => ?_)
 224              refine Finset.sum_congr rfl (fun j _ => ?_)
 225              ring
 226      _ =
 227        (∑ i : Fin n, ∑ j : Fin n,
 228          G.weight i j * (ε i - ε j) ^ 2)
 229          + (∑ i : Fin n, ∑ j : Fin n,
 230            (2 * t) *
 231              (G.weight i j * (ε i - ε j) * (η i - η j)))
 232          + (∑ i : Fin n, ∑ j : Fin n,
 233            t ^ 2 * (G.weight i j * (η i - η j) ^ 2)) := by
 234              simp only [Finset.sum_add_distrib]
 235      _ =
 236        (∑ i : Fin n, ∑ j : Fin n,
 237          G.weight i j * (ε i - ε j) ^ 2)
 238          + 2 * t * (∑ i : Fin n, ∑ j : Fin n,
 239            G.weight i j * (ε i - ε j) * (η i - η j))
 240          + t ^ 2 * (∑ i : Fin n, ∑ j : Fin n,
 241            G.weight i j * (η i - η j) ^ 2) := by
 242              rw [double_sum_mul_left (n := n) (c := 2 * t)]
 243              rw [double_sum_mul_left (n := n) (c := t ^ 2)]
 244  unfold laplacian_action
 245  rw [hsum]
 246  rw [← laplacian_bilinear_eq_pairing G ε η]
 247  unfold laplacian_bilinear
 248  ring
 249
 250/-! ## Unit dipole consequences -/
 251
 252/-- The unit source at `a` paired with the unit sink at `b`. -/
 253def unitDipole {n : ℕ} (a b : Fin n) (i : Fin n) : ℝ :=
 254  (if i = a then 1 else 0) - (if i = b then 1 else 0)
 255
 256/-- Pairing a field with a unit dipole gives its potential drop. -/
 257theorem sum_mul_unitDipole {n : ℕ} (ε : Fin n → ℝ) (a b : Fin n) :
 258    (∑ i : Fin n, ε i * unitDipole a b i) = ε a - ε b := by
 259  unfold unitDipole
 260  simp [mul_sub, Finset.sum_sub_distrib]
 261
 262/-- If the Laplacian is a unit dipole, the action is the potential drop. -/
 263theorem laplacian_action_eq_potential_drop_of_eq_unitDipole {n : ℕ}
 264    (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) (a b : Fin n)
 265    (hsource : ∀ i, discrete_laplacian G ε i = unitDipole a b i) :
 266    laplacian_action G ε = ε a - ε b := by
 267  rw [laplacian_action_eq_pairing]
 268  unfold laplacian_pairing
 269  calc
 270    (∑ i : Fin n, ε i * discrete_laplacian G ε i)
 271        = ∑ i : Fin n, ε i * unitDipole a b i := by
 272            refine Finset.sum_congr rfl (fun i _ => ?_)
 273            rw [hsource i]
 274    _ = ε a - ε b := sum_mul_unitDipole ε a b
 275
 276/-- If twice the Laplacian is a unit dipole, the action is half the
 277potential drop. This is the alternative normalization exposed by the forced
 278coefficient `2` in the action variation. -/
 279theorem laplacian_action_eq_half_potential_drop_of_two_eq_unitDipole {n : ℕ}
 280    (G : WeightedLedgerGraph n) (ε : Fin n → ℝ) (a b : Fin n)
 281    (hsource : ∀ i, 2 * discrete_laplacian G ε i = unitDipole a b i) :
 282    laplacian_action G ε = (ε a - ε b) / 2 := by
 283  rw [laplacian_action_eq_pairing]
 284  unfold laplacian_pairing
 285  have hhalf : ∀ i, discrete_laplacian G ε i = (1 / 2 : ℝ) * unitDipole a b i := by
 286    intro i
 287    linarith [hsource i]
 288  calc
 289    (∑ i : Fin n, ε i * discrete_laplacian G ε i)
 290        = ∑ i : Fin n, ε i * ((1 / 2 : ℝ) * unitDipole a b i) := by
 291            refine Finset.sum_congr rfl (fun i _ => ?_)
 292            rw [hhalf i]
 293    _ = (1 / 2 : ℝ) * ∑ i : Fin n, ε i * unitDipole a b i := by
 294          rw [Finset.mul_sum]
 295          refine Finset.sum_congr rfl (fun i _ => ?_)
 296          ring
 297    _ = (ε a - ε b) / 2 := by
 298          rw [sum_mul_unitDipole]
 299          ring
 300
 301end
 302
 303end ContinuumBridge
 304end SimplicialLedger
 305end Foundation
 306end IndisputableMonolith
 307