Foundation Pair Kernel Discrete Gauss Sum Div F Region Eq Boundary Flux

Discrete Gauss Law

Gauss's theorem is one of the most useful facts in physics: the total amount of something produced inside a region equals the amount that flows out through the region's boundary. Think of a room with people entering and leaving through doors. If no one appears or vanishes inside, the number entering through the doors must equal the number leaving. The theorem being described here is the discrete, finite version of that idea, stated for a network of points rather than a continuous space.

In this discrete setting, the production at each point is called the divergence, which is a measure of net outflow: the sum of all flows leaving a point minus those entering it. The theorem, named sum_divF_region_eq_boundary_flux, states that for any region S in the network, the sum of divergences inside S equals the sum of flows from points in S to points outside S. This is the discrete analogue of the classical divergence theorem, and it holds for any antisymmetric current, meaning any assignment of flows where the flow from i to j is exactly the negative of the flow from j to i.

The key assumption is antisymmetry, which is the mathematical expression of double-entry bookkeeping: every debit at one account is a matching credit at another. The framework models a recognition event as such a posting, where a flow of +1 goes from one site to another and a flow of -1 goes back. This structure is what makes the theorem non-trivial. A uniform flow of 1 between every pair of points, which is not antisymmetric, has a total divergence of n², not zero, showing that antisymmetry is essential and the theorem has real content.

In Recognition Science, this theorem is part of a chain that derives physical structure from the cost of recognition events. The framework's machine-checked library proves it as a formal theorem, and it establishes that the recognition current obeys a genuine discrete Gauss law. However, the theorem does not claim that the current is a gradient of some potential, nor does it derive the 1/r potential or any specific physical constants. Those are separate, later steps in the framework's development.

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

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

What this page does not claim

The current is not claimed to be a gradient of any potential. The theorem does not derive the 1/r potential or any specific physical constants. Antisymmetry is necessary, but the theorem does not claim it is sufficient for all physical conservation laws.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PairKernelDiscreteGauss.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: