IndisputableMonolith.Foundation.PairKernelDiscreteGauss
Develops the discrete double-entry structure for recognition currents: pair-flow antisymmetry alone forces global conservation and a discrete Gauss theorem (sum of divergences equals boundary flux). Cited by anyone in the pair-kernel or metric-edge gravity lane. Proofs are elementary finite-sum identities; gradient structure is not required.
claimA recognition current $F$ on pairs is antisymmetric when $F(i,j)=-F(j,i)$. Its discrete divergence is $\mathrm{div}\,F(i)=\sum_j F(i,j)$. Antisymmetry implies $\sum_i \mathrm{div}\,F(i)=0$ and the region identity $\sum_{i\in R}\mathrm{div}\,F(i)=$ boundary flux. Constant non-antisymmetric flows break conservation. Elementary postings are the basic antisymmetric ledger moves.
background
Recognition Science treats ledger exchange as a pair current on a discrete graph. The module sits under Door 2 / L0 locality (finite-range weight graph) from PairKernelLocality: the provenance lane that isolates on-site exclusion and the ratio bridge without yet committing to the full continuum bridge.
Double-entry is stated purely as antisymmetry: flow $i\to j$ equals minus flow $j\to i$. That is the bookkeeping content of "every debit has a matching credit" at the elementary current. A gradient $F(i,j)=\varphi_i-\varphi_j$ is one instance, but none of the conservation theorems need the gradient form.
Notation introduced here: IsAntisym for the antisymmetry predicate; divF for the discrete divergence; elementaryPosting for the basic antisymmetric move; counterexamples via constant flows that are not antisymmetric and therefore break global sum-to-zero.
proof idea
Definition-and-lemma module, not a single deep theorem. Antisymmetry is recorded as a predicate; divergence is the obvious site sum. Finite double-counting then gives: sum of an antisymmetric kernel over a Finset vanishes, hence total sum of divF is zero. The region form rewrites the interior sum as a boundary flux by the same pairing. Constant flows are exhibited as non-antisymmetric with nonzero total divergence, so conservation is sharp. Elementary postings are checked to be antisymmetric by direct evaluation. No analytic estimates; pure finite combinatorics.
why it matters in Recognition Science
Supplies the discrete conservation backbone that gravity analysis imports when reading strain currents on the Freudenthal patch. Downstream, MetricEdgeImage4D treats a finite linearized metric edge image: $F$ as strain current of a Mat4 perturbation on the sixteen-site patch, matching the frozen world metric-null plan. Without antisymmetry-level Gauss, edge-image conservation and boundary matching would be ad hoc.
In the foundation chain this is the double-entry half of the pair-kernel story (locality upstream, discrete Gauss here). It separates bookkeeping from dynamics: RCL and J-cost live elsewhere; here only the signed ledger identity is forced. That split keeps later continuum or continuum-limit claims from smuggling conservation in as a modeling choice.
scope and limits
- Does not assume or prove that currents are gradients of a potential.
- Does not derive the Recognition Composition Law or J-uniqueness (T5).
- Does not fix continuum limits, continuum Gauss, or continuum Stokes forms.
- Does not encode locality range; that lives in the upstream PairKernelLocality module.
- Does not construct the metric edge image; only feeds conservation structure downstream.
used by (1)
depends on (1)
declarations in this module (16)
-
def
IsAntisym -
def
divF -
def
constFlow -
theorem
constFlow_not_antisym -
theorem
constFlow_sum_div -
theorem
constFlow_breaks_conservation -
theorem
antisym_sum_finset_zero -
theorem
sum_divF_zero -
theorem
sum_divF_region_eq_boundary_flux -
theorem
sigma_sum_zero_of_continuity -
def
elementaryPosting -
theorem
elementaryPosting_antisym -
theorem
elementaryPosting_sum_div_zero -
theorem
elementaryPosting_div_source -
theorem
elementaryPosting_div_sink -
theorem
elementaryPosting_divF_eq_unitDipole