Foundation Pair Kernel Discrete Gauss Sigma Sum Zero Of Continuity

/-- The elementary current of a single recognition posting from account `a` to account `b`:
    `+1` on the ordered pair `(a,b)`, `−1` on `(b,a)`, `0` elsewhere. This is the double-entry
    structure of one recognition event, built from postings, NOT from a potential. -/
def elementaryPosting {n : ℕ} (a b : Fin n) : Fin n → Fin n → ℝ :=
  fun i j => (if i = a ∧ j = b then (1 : ℝ) else 0) - (if i = b ∧ j = a then (1 : ℝ) else 0)

/-- **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]

/-- **Double-entry structure.** A recognition current is antisymmetric: the flow from `i` to `j` is
    minus the flow from `j` to `i`. This is exactly what "every debit has a matching credit" means
    at the level of the elementary current. It is NOT the gradient condition; a gradient
    `F i j = φ i − φ j` is one instance, but the theorems below use only antisymmetry. -/
def IsAntisym {n : ℕ} (F : Fin n → Fin n → ℝ) : Prop := ∀ i j, F i j = - F j i

/-- **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)

/-- **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'

/-- **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]