Foundation Pair Kernel Discrete Gauss Elementary Posting Div F Eq Unit Dipole

The posting as a unit dipole

In the Recognition Science framework, a ledger is a discrete record of events, and each event is a recognition between two sites. The framework represents the simplest possible event, a single posting from account a to account b, as a flow: a positive unit of current from a to b, a negative unit from b to a, and zero everywhere else. This flow is antisymmetric: the current from i to j is always the negative of the current from j to i, which is the double-entry structure of a recognition event, where every debit at one account is a matching credit at another.

The declaration elementaryPosting_divF_eq_unitDipole proves that the divergence of this elementary posting is exactly the unit dipole, a source pattern that is plus one at the posting's origin and minus one at its destination. The divergence measures the net outflow from a site, so the theorem states that a single posting creates a source of strength one at a and a sink of strength one at b, with nothing elsewhere. This holds for any pair of sites, including the degenerate case where a equals b. The result identifies the source of the recognition current with the source used in the finite Dirichlet action, a classical energy functional, bridging the discrete ledger structure to a continuum description.

This theorem is part of a chain that establishes a discrete Gauss law: for any antisymmetric current on a finite lattice, the total source over the whole lattice is zero, and the source within a region equals the flux through its boundary. The elementary posting is the concrete witness that this structure is realizable, not just a formal possibility. The framework's machine-checked library of formal theorems proves these statements with no unproved assumptions beyond the standard logical axioms.

The theorem does not claim that the recognition current is a gradient of a potential. The flow is kept abstract, free to be any antisymmetric current, and the Gauss law holds for all of them. It also does not derive the inverse-square law or any specific force law; that is a later step requiring the Green's function of the resulting Laplacian. The theorem says nothing about the numerical constants that appear elsewhere in the framework, such as 5/8 or 27/16, nor about any hydrogenic potential. Its content is purely structural: the double-entry posting is the unit dipole source.

/-- The divergence of an elementary posting is exactly the independently defined unit dipole.
    This identifies the recognition-current source with the source used by the finite
    Dirichlet action, including the degenerate case `a = b`. -/
theorem elementaryPosting_divF_eq_unitDipole {n : ℕ} (a b i : Fin n) :
    divF (elementaryPosting a b) i =
      SimplicialLedger.ContinuumBridge.unitDipole a b i := by
  unfold divF elementaryPosting SimplicialLedger.ContinuumBridge.unitDipole
  have hforward :
      (∑ j : Fin n, if i = a ∧ j = b then (1 : ℝ) else 0) =
        if i = a then 1 else 0 := by
    by_cases hia : i = a
    · subst i
      simp
    · simp [hia]
  have hbackward :
      (∑ j : Fin n, if i = b ∧ j = a then (1 : ℝ) else 0) =
        if i = b then 1 else 0 := by
    by_cases hib : i = b
    · subst i
      simp
    · simp [hib]
  rw [Finset.sum_sub_distrib, hforward, hbackward]

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

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

What this page does not claim

The recognition current is a gradient of a potential. The inverse-square law or any specific force law is derived from this theorem. The numerical constants 5/8, 5/16, 27/16, or Z_eff appear in this result.

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: