Foundation Pair Kernel Source Variation Action Eq Half Potential Drop Of Two Lap

The half-drop identity

In the mathematics of weighted graphs, a ledger (a discrete record of values at vertices) assigns a number to each point, and a symmetric weight measures the connection strength between pairs. The action (a sum of squared differences, weighted by connection strength) quantifies how much the values vary across the graph. The theorem action_eq_half_potential_drop_of_two_laplacian_eq_dipole states a precise relation: if the graph Laplacian (the operator measuring how a value differs from its neighbors) equals half of a unit dipole (a field that is +1 at one point, -1 at another, and 0 elsewhere), then the action equals half the difference of the field values at those two points.

This identity is a direct consequence of the symmetry of the weights, and it is proved in the machine-checked library of formal theorems. The proof uses the exact line expansion of the action, which shows that the first variation coefficient is exactly 2, and the Dirichlet identity, which relates the action to the sum of the field times its Laplacian. The result is algebraic and exact: it holds for any finite set of vertices, any symmetric weights, and any real-valued field, with no approximation or limiting argument.

In Recognition Science, this theorem is a building block in the framework's account of how a discrete ledger gives rise to continuous physical structure. It is a mathematical model input, not a physical law: the action is defined, not derived, and the identity does not select any additional physical source scale. The theorem establishes a clean relation within the model, but it does not by itself say that any physical system obeys this equation.

The practical consequence is a bridge between two ways of describing a field: the global energy (the action) and the local source (the Laplacian). When the source is a dipole, the energy is simply half the potential drop, a compact formula that connects the ledger's global cost to a local difference. This is the kind of exact structural fact that the framework uses to build larger derivations, though the physical interpretation of the ledger itself remains a separate question.

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

/-- The derivative of the action along a line has coefficient `2`. -/
theorem action_hasDerivAt_line
    (w : ι → ι → ℝ) (e v : ι → ℝ) :
    HasDerivAt
      (fun t : ℝ => action w (fun i => e i + t * v i))
      (2 * dirichlet w e v)
      0 := by
  have hfun :
      (fun t : ℝ => action w (fun i => e i + t * v i))
        = fun t : ℝ => action w e + 2 * t * dirichlet w e v
            + t ^ 2 * action w v := by
    funext t
    exact action_line_expansion w e v t
  rw [hfun]
  convert
    ((hasDerivAt_const (x := (0 : ℝ)) (action w e)).add
      (((hasDerivAt_id (𝕜 := ℝ) (x := (0 : ℝ))).const_mul 2).mul_const
        (dirichlet w e v))).add
      (((hasDerivAt_id (𝕜 := ℝ) (x := (0 : ℝ))).pow 2).mul_const (action w v))
    using 1
  all_goals norm_num [id]

/-- The symmetric weighted quadratic pair action. -/
def action (w : ι → ι → ℝ) (e : ι → ℝ) : ℝ :=
  (1 / 2 : ℝ) * ∑ i, ∑ j, w i j * (e i - e j) ^ 2

What this page does not claim

The theorem does not claim that any physical system actually has a Laplacian equal to a dipole. It does not derive the action from more basic principles; the action is a definitional choice. It does not select a physical scale for the source, as the docstring explicitly states.

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: