Foundation Pair Kernel Source Variation Action Eq Potential Drop Of Laplacian Eq

The dipole identity

In the mathematics of networks, a ledger, a discrete record of values at connected points, often assigns an energy to a field. The declaration concerns a specific quadratic energy: half the sum over all pairs of points of the weight between them times the squared difference of their field values. This is the Dirichlet form on a weighted graph, a standard object that measures how much a field varies across the connections.

The key identity, proved in the machine-checked library of formal theorems, states a clean equivalence. If the weighted graph Laplacian of a field equals a unit dipole, meaning it has value +1 at one point, -1 at another, and 0 elsewhere, then the field's energy equals the difference between the field's values at those two points. In symbols: when Δe = δ_a - δ_b, then A(e) = e(a) - e(b). This is a theorem, not a definition.

The proof rests on two earlier results. First, the energy equals the sum over points of the field times its Laplacian, which follows from symmetry of the weights. Second, pairing any field with a unit dipole extracts exactly the potential drop, the difference in field values between the two poles. Combining these gives the result directly, with no limiting argument and no additional assumptions beyond symmetry and the dipole condition.

In Recognition Science, this identity is a bridge: it shows that when a source takes the simplest possible form, a single unit charge paired with a unit sink, the energy collapses to a simple difference. The framework models this as a foundational algebraic fact about how sources and fields interact. The declaration also records a companion result: if twice the Laplacian equals a unit dipole, the energy is half the potential drop.

The declaration does not claim that any physical system actually has a dipole Laplacian. It does not select a physical source scale, and it does not derive the fine-structure constant or any other coupling. It is a mathematical model input, a clean algebraic identity that holds for any symmetric weighted graph, waiting for a physical interpretation that the framework does not supply here.

/-- If the Laplacian is a unit dipole, the energy is the potential drop. -/
theorem action_eq_potential_drop_of_laplacian_eq_dipole
    [DecidableEq ι]
    (w : ι → ι → ℝ) (e : ι → ℝ) (a b : ι)
    (hsymm : ∀ i j, w i j = w j i)
    (hsource : ∀ i, laplacian w e i = dipole a b i) :
    action w e = e a - e b := by
  rw [action_eq_sum_mul_laplacian w e hsymm]
  calc
    (∑ i, e i * laplacian w e i) = ∑ i, e i * dipole a b i := by
      apply Finset.sum_congr rfl
      intro i _
      rw [hsource i]
    _ = e a - e b := sum_mul_dipole e a b

/-- Kernel-clean energy identity: `A(e) = ∑ᵢ eᵢ (Δe)ᵢ`. -/
theorem action_eq_sum_mul_laplacian
    (w : ι → ι → ℝ) (e : ι → ℝ)
    (hsymm : ∀ i j, w i j = w j i) :
    action w e = ∑ i, e i * laplacian w e i := by
  rw [action_eq_dirichlet_self]
  exact dirichlet_eq_sum_mul_laplacian w e e hsymm

/-- Pairing any field with a unit dipole gives its potential drop. -/
theorem sum_mul_dipole [DecidableEq ι] (e : ι → ℝ) (a b : ι) :
    (∑ i, e i * dipole a b i) = e a - e b := by
  unfold dipole
  simp [mul_sub, Finset.sum_sub_distrib]

/-- If twice the Laplacian is a unit dipole, the energy is half the
potential drop. -/
theorem action_eq_half_potential_drop_of_two_laplacian_eq_dipole
    [DecidableEq ι]
    (w : ι → ι → ℝ) (e : ι → ℝ) (a b : ι)
    (hsymm : ∀ i j, w i j = w j i)
    (hsource : ∀ i, 2 * laplacian w e i = dipole a b i) :
    action w e = (e a - e b) / 2 := by
  rw [action_eq_sum_mul_laplacian w e hsymm]
  have hhalf : ∀ i, laplacian w e i = (1 / 2 : ℝ) * dipole a b i := by
    intro i
    linarith [hsource i]
  calc
    (∑ i, e i * laplacian w e i)
        = ∑ i, e i * ((1 / 2 : ℝ) * dipole a b i) := by
          apply Finset.sum_congr rfl
          intro i _
          rw [hhalf i]
    _ = ∑ i, (1 / 2 : ℝ) * (e i * dipole a b i) := by
          apply Finset.sum_congr rfl
          intro i _
          ring
    _ = (1 / 2 : ℝ) * ∑ i, e i * dipole a b i := by
          rw [Finset.mul_sum]
    _ = (e a - e b) / 2 := by
          rw [sum_mul_dipole]
          ring

What this page does not claim

No physical system is asserted to have a dipole Laplacian. No physical source scale is selected by these identities. No claim is made about the fine-structure constant or any other coupling.

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/PairKernelSourceVariation.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: