IndisputableMonolith.Foundation.PairKernelDiscreteGauss

   1import IndisputableMonolith.Foundation.PairKernelLocality
   2
   3/-!
   4# Door 2 / discrete Gauss: recognition flux, site-divergence = sigma-imbalance
   5
   6Pair-kernel provenance lane (`glm/fold_derivation_logs/pairwise_kernel_derive.md`).
   7
   8After the pair-cost carrier (`ShiftInvariant`, MODEL-terminal) and the locality hypothesis
   9(`FiniteRange`, HYPOTHESIS; atomic-tick provenance CLOSED NEGATIVE), the next vertebra is the
  10discrete Gauss / continuity law: the divergence of the recognition current equals the local
  11sigma-imbalance, and integrating over the lattice gives zero net source (the sigma = 0 conservation
  12law), with the regional form giving source-in-region = flux-through-boundary.
  13
  14## The vacuity trap, and the null test built FIRST
  15
  16The trap the lane flags explicitly: if one *defines* the current as a gradient `F i j := φ i − φ j`
  17and the source as the graph Laplacian `Δφ`, then "divergence = source" is the identity
  18`Δφ = div (∇φ)` — a tautology that says nothing about double-entry and carries no conservation
  19content (it holds for every `φ`). So the flux is kept ABSTRACT here: `F : Fin n → Fin n → ℝ` is a
  20free antisymmetric current, never `∇φ`. The real content is CONSERVATION, and it holds *because* the
  21current is antisymmetric (`F i j = − F j i`), which is exactly the double-entry structure of a
  22recognition event (each debit at one account is a matching credit at another).
  23
  24Reviewer vacuity check, run before the theorems: is global conservation `∑ divF = 0` a null test
  25(true for every flow)? No. `constFlow_breaks_conservation` shows a non-antisymmetric flow
  26(`F ≡ 1`) has `∑ divF = n² ≠ 0`. So antisymmetry is load-bearing; the Gauss law has teeth. This is
  27the null test built first, and it passes (instrument informative).
  28
  29## What is proved (all axiom-clean)
  30
  31- `antisym_sum_finset_zero`: over any region `S`, an antisymmetric current sums to zero
  32  (`∑_{i∈S} ∑_{j∈S} F i j = 0`). The double-entry cancellation, the engine of everything below.
  33- `sum_divF_zero` (**global Gauss**): `∑ i, divF F i = 0`. Net recognition source over the whole
  34  lattice is zero — the sigma = 0 neutrality, forced by antisymmetry.
  35- `sum_divF_region_eq_boundary_flux` (**regional Gauss / divergence theorem**):
  36  `∑_{i∈S} divF F i = ∑_{i∈S} ∑_{j∈Sᶜ} F i j`. Source in a region equals flux through its boundary.
  37  This is the genuine (non-tautological) discrete divergence theorem: it holds for ANY antisymmetric
  38  current, gradient or not, so it is not a statement about `∇φ`.
  39- `sigma_sum_zero_of_continuity`: if a source `sigma` satisfies the continuity law `divF F = sigma`
  40  for an antisymmetric current, then `∑ sigma = 0`. This is "site-divergence = sigma-imbalance ⇒
  41  global sigma neutrality" without ever writing `sigma := Δφ`.
  42- `elementaryPosting` + `_antisym` + `_sum_div_zero` + `_div_source`: the double-entry witness — a
  43  single a→b posting is an antisymmetric current whose divergence is `+1` at `a` and `−1` at `b`
  44  (the concrete debit/credit source), and it conserves globally.
  45- Decoy `constFlow` + `constFlow_not_antisym` + `constFlow_breaks_conservation`: the null test.
  46
  47## Scoped verdict (`inference-discipline.mdc` form)
  48
  49- CLAIM: for any antisymmetric recognition current on a finite lattice, the divergence obeys the
  50  discrete Gauss law (global net source zero; regional source = boundary flux), and a source it
  51  realizes is globally neutral. Antisymmetry (double-entry) is necessary (`constFlow` decoy).
  52- DOMAIN: currents `F : Fin n → Fin n → ℝ`; `divF F i = ∑ j, F i j`; regions `S : Finset (Fin n)`.
  53- PREMISES: `IsAntisym F` (double-entry) [the modelled structure of a recognition event; a single
  54  posting realizes it, `elementaryPosting_antisym`].
  55- REACH: max licensed → "the recognition current obeys a genuine discrete Gauss law; global sigma is
  56  conserved by double-entry; source in a region = boundary flux." Does NOT license → `1/r` from this
  57  alone (that is L4, the Green's function of the resulting Laplacian), nor that the current is a
  58  gradient (`F` is free antisymmetric), nor any use of `5/8`, `5/16`, `27/16`, `Z_eff`, hydrogenic
  59  `F(r)` (none appear here).
  60
  61Zero `sorry`. Zero new `axiom`.
  62-/
  63
  64namespace IndisputableMonolith
  65namespace Foundation
  66namespace PairKernelDiscreteGauss
  67
  68open Finset
  69
  70noncomputable section
  71
  72/-! ## §1. The recognition current and its divergence -/
  73
  74/-- **Double-entry structure.** A recognition current is antisymmetric: the flow from `i` to `j` is
  75    minus the flow from `j` to `i`. This is exactly what "every debit has a matching credit" means
  76    at the level of the elementary current. It is NOT the gradient condition; a gradient
  77    `F i j = φ i − φ j` is one instance, but the theorems below use only antisymmetry. -/
  78def IsAntisym {n : ℕ} (F : Fin n → Fin n → ℝ) : Prop := ∀ i j, F i j = - F j i
  79
  80/-- Site divergence: the net recognition outflow from site `i`. -/
  81def divF {n : ℕ} (F : Fin n → Fin n → ℝ) (i : Fin n) : ℝ := ∑ j : Fin n, F i j
  82
  83/-! ## §2. Null test (built first): antisymmetry is load-bearing
  84
  85The uniform current `F ≡ 1` is NOT antisymmetric, and it does NOT conserve: `∑ divF = n²`. So the
  86global Gauss law below is not a null test — deleting the antisymmetry hypothesis lets a
  87non-conserving flow stand. -/
  88
  89/-- The uniform (all-ones) current — a decoy that is not double-entry. -/
  90def constFlow (n : ℕ) : Fin n → Fin n → ℝ := fun _ _ => 1
  91
  92theorem constFlow_not_antisym (n : ℕ) (hn : 0 < n) : ¬ IsAntisym (constFlow n) := by
  93  intro h
  94  have hii := h ⟨0, hn⟩ ⟨0, hn⟩
  95  simp only [constFlow] at hii
  96  norm_num at hii
  97
  98theorem constFlow_sum_div (n : ℕ) :
  99    ∑ i : Fin n, divF (constFlow n) i = (n : ℝ) * (n : ℝ) := by
 100  simp only [divF, constFlow, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
 101    nsmul_eq_mul, mul_one]
 102
 103/-- **Null test passes.** A non-antisymmetric current breaks global conservation
 104    (`∑ divF ≠ 0`). So the double-entry hypothesis is load-bearing in the Gauss law. -/
 105theorem constFlow_breaks_conservation (n : ℕ) (hn : 0 < n) :
 106    ∑ i : Fin n, divF (constFlow n) i ≠ 0 := by
 107  rw [constFlow_sum_div]
 108  have hpos : (0 : ℝ) < (n : ℝ) := by exact_mod_cast hn
 109  exact (mul_pos hpos hpos).ne'
 110
 111/-! ## §3. The double-entry cancellation, over an arbitrary region -/
 112
 113/-- Over any region `S`, an antisymmetric current sums to zero: the double-entry cancellation.
 114    This is the engine of both the global and regional Gauss laws. -/
 115theorem antisym_sum_finset_zero {n : ℕ} {F : Fin n → Fin n → ℝ} (h : IsAntisym F)
 116    (S : Finset (Fin n)) : ∑ i ∈ S, ∑ j ∈ S, F i j = 0 := by
 117  have hcomm : (∑ i ∈ S, ∑ j ∈ S, F j i) = ∑ i ∈ S, ∑ j ∈ S, F i j := Finset.sum_comm
 118  have hzero : (∑ i ∈ S, ∑ j ∈ S, (F i j + F j i)) = 0 := by
 119    apply Finset.sum_eq_zero
 120    intro i _
 121    apply Finset.sum_eq_zero
 122    intro j _
 123    have := h i j
 124    linarith
 125  have hsplit : (∑ i ∈ S, ∑ j ∈ S, (F i j + F j i))
 126      = (∑ i ∈ S, ∑ j ∈ S, F i j) + (∑ i ∈ S, ∑ j ∈ S, F j i) := by
 127    rw [← Finset.sum_add_distrib]
 128    apply Finset.sum_congr rfl
 129    intro i _
 130    rw [Finset.sum_add_distrib]
 131  rw [hsplit, hcomm] at hzero
 132  linarith
 133
 134/-! ## §4. Global and regional discrete Gauss -/
 135
 136/-- **Global discrete Gauss.** The total recognition source over the whole lattice is zero: the
 137    sigma = 0 conservation law, forced by double-entry antisymmetry (not by any `φ`). -/
 138theorem sum_divF_zero {n : ℕ} {F : Fin n → Fin n → ℝ} (h : IsAntisym F) :
 139    ∑ i : Fin n, divF F i = 0 := by
 140  simp only [divF]
 141  simpa using antisym_sum_finset_zero h (Finset.univ)
 142
 143/-- **Regional discrete Gauss (divergence theorem).** Source in a region `S` equals the flux
 144    through its boundary: `∑_{i∈S} divF F i = ∑_{i∈S} ∑_{j∈Sᶜ} F i j`. Holds for ANY antisymmetric
 145    current — gradient or circulating — so it is not a statement about `∇φ`. -/
 146theorem sum_divF_region_eq_boundary_flux {n : ℕ} {F : Fin n → Fin n → ℝ} (h : IsAntisym F)
 147    (S : Finset (Fin n)) :
 148    ∑ i ∈ S, divF F i = ∑ i ∈ S, ∑ j ∈ Sᶜ, F i j := by
 149  have hsplit : ∀ i, divF F i = (∑ j ∈ S, F i j) + (∑ j ∈ Sᶜ, F i j) := by
 150    intro i
 151    rw [divF, ← Finset.sum_add_sum_compl S (fun j => F i j)]
 152  calc ∑ i ∈ S, divF F i
 153      = ∑ i ∈ S, ((∑ j ∈ S, F i j) + (∑ j ∈ Sᶜ, F i j)) := by
 154        apply Finset.sum_congr rfl; intro i _; exact hsplit i
 155    _ = (∑ i ∈ S, ∑ j ∈ S, F i j) + (∑ i ∈ S, ∑ j ∈ Sᶜ, F i j) := by
 156        rw [Finset.sum_add_distrib]
 157    _ = 0 + (∑ i ∈ S, ∑ j ∈ Sᶜ, F i j) := by rw [antisym_sum_finset_zero h S]
 158    _ = ∑ i ∈ S, ∑ j ∈ Sᶜ, F i j := by rw [zero_add]
 159
 160/-- **Continuity ⇒ global neutrality.** If a source `sigma` is the divergence of an antisymmetric
 161    current (`divF F = sigma`, the Gauss law "site-divergence = sigma-imbalance"), then the total
 162    source is zero. This is the sigma = 0 conservation law stated on the source, with no `sigma :=
 163    Δφ` definitional shortcut. -/
 164theorem sigma_sum_zero_of_continuity {n : ℕ} {F : Fin n → Fin n → ℝ} {sigma : Fin n → ℝ}
 165    (h : IsAntisym F) (hcont : ∀ i, divF F i = sigma i) :
 166    ∑ i : Fin n, sigma i = 0 := by
 167  have : ∑ i : Fin n, sigma i = ∑ i : Fin n, divF F i := by
 168    apply Finset.sum_congr rfl
 169    intro i _
 170    exact (hcont i).symm
 171  rw [this, sum_divF_zero h]
 172
 173/-! ## §5. The double-entry witness: a single posting is an antisymmetric current -/
 174
 175/-- The elementary current of a single recognition posting from account `a` to account `b`:
 176    `+1` on the ordered pair `(a,b)`, `−1` on `(b,a)`, `0` elsewhere. This is the double-entry
 177    structure of one recognition event, built from postings, NOT from a potential. -/
 178def elementaryPosting {n : ℕ} (a b : Fin n) : Fin n → Fin n → ℝ :=
 179  fun i j => (if i = a ∧ j = b then (1 : ℝ) else 0) - (if i = b ∧ j = a then (1 : ℝ) else 0)
 180
 181theorem elementaryPosting_antisym {n : ℕ} (a b : Fin n) : IsAntisym (elementaryPosting a b) := by
 182  intro i j
 183  unfold elementaryPosting
 184  have c1 : (j = b ∧ i = a) ↔ (i = a ∧ j = b) := and_comm
 185  have c2 : (j = a ∧ i = b) ↔ (i = b ∧ j = a) := and_comm
 186  simp only [c1, c2]
 187  ring
 188
 189/-- A single posting conserves globally (it is antisymmetric). -/
 190theorem elementaryPosting_sum_div_zero {n : ℕ} (a b : Fin n) :
 191    ∑ i : Fin n, divF (elementaryPosting a b) i = 0 :=
 192  sum_divF_zero (elementaryPosting_antisym a b)
 193
 194/-- The divergence of the elementary a→b posting is `+1` at the source `a` (for `a ≠ b`): the
 195    concrete debit at `a`. Together with the `−1` at `b` this is the sigma-imbalance the current
 196    carries — the double-entry source, read off the postings, not off `∇φ`. -/
 197theorem elementaryPosting_div_source {n : ℕ} (a b : Fin n) (hab : a ≠ b) :
 198    divF (elementaryPosting a b) a = 1 := by
 199  have hstep : ∀ j : Fin n,
 200      elementaryPosting a b a j = (if j = b then (1 : ℝ) else 0) := by
 201    intro j
 202    simp only [elementaryPosting]
 203    have hb : (a = b ∧ j = a) → False := fun hc => hab hc.1
 204    rw [if_neg hb]
 205    simp only [true_and, sub_zero]
 206  calc divF (elementaryPosting a b) a
 207      = ∑ j : Fin n, elementaryPosting a b a j := rfl
 208    _ = ∑ j : Fin n, (if j = b then (1 : ℝ) else 0) := by
 209          exact Finset.sum_congr rfl (fun j _ => hstep j)
 210    _ = 1 := by simp
 211
 212theorem elementaryPosting_div_sink {n : ℕ} (a b : Fin n) (hab : a ≠ b) :
 213    divF (elementaryPosting a b) b = -1 := by
 214  have hstep : ∀ j : Fin n,
 215      elementaryPosting a b b j = (if j = a then (-1 : ℝ) else 0) := by
 216    intro j
 217    simp only [elementaryPosting]
 218    have ha : (b = a ∧ j = b) → False := fun hc => hab hc.1.symm
 219    rw [if_neg ha]
 220    by_cases hja : j = a
 221    · subst hja; simp
 222    · simp [hja]
 223  calc divF (elementaryPosting a b) b
 224      = ∑ j : Fin n, elementaryPosting a b b j := rfl
 225    _ = ∑ j : Fin n, (if j = a then (-1 : ℝ) else 0) := by
 226          exact Finset.sum_congr rfl (fun j _ => hstep j)
 227    _ = -1 := by simp
 228
 229/-- The divergence of an elementary posting is exactly the independently defined unit dipole.
 230    This identifies the recognition-current source with the source used by the finite
 231    Dirichlet action, including the degenerate case `a = b`. -/
 232theorem elementaryPosting_divF_eq_unitDipole {n : ℕ} (a b i : Fin n) :
 233    divF (elementaryPosting a b) i =
 234      SimplicialLedger.ContinuumBridge.unitDipole a b i := by
 235  unfold divF elementaryPosting SimplicialLedger.ContinuumBridge.unitDipole
 236  have hforward :
 237      (∑ j : Fin n, if i = a ∧ j = b then (1 : ℝ) else 0) =
 238        if i = a then 1 else 0 := by
 239    by_cases hia : i = a
 240    · subst i
 241      simp
 242    · simp [hia]
 243  have hbackward :
 244      (∑ j : Fin n, if i = b ∧ j = a then (1 : ℝ) else 0) =
 245        if i = b then 1 else 0 := by
 246    by_cases hib : i = b
 247    · subst i
 248      simp
 249    · simp [hib]
 250  rw [Finset.sum_sub_distrib, hforward, hbackward]
 251
 252end
 253
 254end PairKernelDiscreteGauss
 255end Foundation
 256end IndisputableMonolith
 257