Foundation Pair Kernel Discrete Gauss

/-- **Global discrete Gauss.** The total recognition source over the whole lattice is zero: the
    sigma = 0 conservation law, forced by double-entry antisymmetry (not by any `φ`). -/
theorem sum_divF_zero {n : ℕ} {F : Fin n → Fin n → ℝ} (h : IsAntisym F) :
    ∑ i : Fin n, divF F i = 0 := by
  simp only [divF]
  simpa using antisym_sum_finset_zero h (Finset.univ)

/-- **Regional discrete Gauss (divergence theorem).** Source in a region `S` equals the flux
    through its boundary: `∑_{i∈S} divF F i = ∑_{i∈S} ∑_{j∈Sᶜ} F i j`. Holds for ANY antisymmetric
    current — gradient or circulating — so it is not a statement about `∇φ`. -/
theorem sum_divF_region_eq_boundary_flux {n : ℕ} {F : Fin n → Fin n → ℝ} (h : IsAntisym F)
    (S : Finset (Fin n)) :
    ∑ i ∈ S, divF F i = ∑ i ∈ S, ∑ j ∈ Sᶜ, F i j := by
  have hsplit : ∀ i, divF F i = (∑ j ∈ S, F i j) + (∑ j ∈ Sᶜ, F i j) := by
    intro i
    rw [divF, ← Finset.sum_add_sum_compl S (fun j => F i j)]
  calc ∑ i ∈ S, divF F i
      = ∑ i ∈ S, ((∑ j ∈ S, F i j) + (∑ j ∈ Sᶜ, F i j)) := by
        apply Finset.sum_congr rfl; intro i _; exact hsplit i
    _ = (∑ i ∈ S, ∑ j ∈ S, F i j) + (∑ i ∈ S, ∑ j ∈ Sᶜ, F i j) := by
        rw [Finset.sum_add_distrib]
    _ = 0 + (∑ i ∈ S, ∑ j ∈ Sᶜ, F i j) := by rw [antisym_sum_finset_zero h S]
    _ = ∑ i ∈ S, ∑ j ∈ Sᶜ, F i j := by rw [zero_add]

/-- **Null test passes.** A non-antisymmetric current breaks global conservation
    (`∑ divF ≠ 0`). So the double-entry hypothesis is load-bearing in the Gauss law. -/
theorem constFlow_breaks_conservation (n : ℕ) (hn : 0 < n) :
    ∑ i : Fin n, divF (constFlow n) i ≠ 0 := by
  rw [constFlow_sum_div]
  have hpos : (0 : ℝ) < (n : ℝ) := by exact_mod_cast hn
  exact (mul_pos hpos hpos).ne'

theorem elementaryPosting_antisym {n : ℕ} (a b : Fin n) : IsAntisym (elementaryPosting a b) := by
  intro i j
  unfold elementaryPosting
  have c1 : (j = b ∧ i = a) ↔ (i = a ∧ j = b) := and_comm
  have c2 : (j = a ∧ i = b) ↔ (i = b ∧ j = a) := and_comm
  simp only [c1, c2]
  ring

/-- The divergence of the elementary a→b posting is `+1` at the source `a` (for `a ≠ b`): the
    concrete debit at `a`. Together with the `−1` at `b` this is the sigma-imbalance the current
    carries — the double-entry source, read off the postings, not off `∇φ`. -/
theorem elementaryPosting_div_source {n : ℕ} (a b : Fin n) (hab : a ≠ b) :
    divF (elementaryPosting a b) a = 1 := by
  have hstep : ∀ j : Fin n,
      elementaryPosting a b a j = (if j = b then (1 : ℝ) else 0) := by
    intro j
    simp only [elementaryPosting]
    have hb : (a = b ∧ j = a) → False := fun hc => hab hc.1
    rw [if_neg hb]
    simp only [true_and, sub_zero]
  calc divF (elementaryPosting a b) a
      = ∑ j : Fin n, elementaryPosting a b a j := rfl
    _ = ∑ j : Fin n, (if j = b then (1 : ℝ) else 0) := by
          exact Finset.sum_congr rfl (fun j _ => hstep j)
    _ = 1 := by simp

theorem elementaryPosting_div_sink {n : ℕ} (a b : Fin n) (hab : a ≠ b) :
    divF (elementaryPosting a b) b = -1 := by
  have hstep : ∀ j : Fin n,
      elementaryPosting a b b j = (if j = a then (-1 : ℝ) else 0) := by
    intro j
    simp only [elementaryPosting]
    have ha : (b = a ∧ j = b) → False := fun hc => hab hc.1.symm
    rw [if_neg ha]
    by_cases hja : j = a
    · subst hja; simp
    · simp [hja]
  calc divF (elementaryPosting a b) b
      = ∑ j : Fin n, elementaryPosting a b b j := rfl
    _ = ∑ j : Fin n, (if j = a then (-1 : ℝ) else 0) := by
          exact Finset.sum_congr rfl (fun j _ => hstep j)
    _ = -1 := by simp

/-- **Continuity ⇒ global neutrality.** If a source `sigma` is the divergence of an antisymmetric
    current (`divF F = sigma`, the Gauss law "site-divergence = sigma-imbalance"), then the total
    source is zero. This is the sigma = 0 conservation law stated on the source, with no `sigma :=
    Δφ` definitional shortcut. -/
theorem sigma_sum_zero_of_continuity {n : ℕ} {F : Fin n → Fin n → ℝ} {sigma : Fin n → ℝ}
    (h : IsAntisym F) (hcont : ∀ i, divF F i = sigma i) :
    ∑ i : Fin n, sigma i = 0 := by
  have : ∑ i : Fin n, sigma i = ∑ i : Fin n, divF F i := by
    apply Finset.sum_congr rfl
    intro i _
    exact (hcont i).symm
  rw [this, sum_divF_zero h]