Foundation Pair Kernel Source Variation Dirichlet Eq Sum Mul Laplacian

The Dirichlet identity

The Dirichlet form is a standard object in mathematics and physics: a way of measuring the energy of a field by summing squared differences between neighboring values. For a finite set of points with weights w between pairs, the form is (1/2)∑_i∑_j w_ij(e_i − e_j)². This measures how much a field e varies across the connections. The graph Laplacian, written Δ_f at a point, is the weighted sum of differences from that point to its neighbors. These two objects appear throughout network theory, spectral graph theory, and the discrete versions of physics equations.

The core identity, proved in the machine-checked library of formal theorems, states that for any symmetric weights (w_ij = w_ji) and any two fields e and f, the Dirichlet form equals ∑_i e_i (Δf)_i. In words: the energy of the pair equals the sum over points of the first field times the Laplacian of the second. This is a discrete version of integration by parts, the same algebraic fact that underlies the classical Dirichlet principle in calculus. The proof uses only the symmetry of the weights and the rearrangement of finite sums; it needs no limiting argument and no extra assumptions.

The identity is the engine behind several exact consequences in the same file. When e equals f, it shows the quadratic action equals ∑_i e_i (Δe)_i, an energy identity. It also yields the exact first variation of the action along a line: the derivative at zero is 2∑_i v_i (Δe)_i, where the coefficient 2 appears without any approximation. And if the Laplacian of a field is a unit dipole (a source at one point and a sink at another), the action equals the potential drop between those points. These results convert a statement about pairwise differences into one about a Laplacian acting on a single field, which is often the form needed for further analysis.

In Recognition Science, this file isolates the algebra forced by a symmetric quadratic pair action. The framework models the action as a mathematical input, not a derived physical law. The identities hold for any symmetric weights and any finite fields; they do not select a particular source scale or coupling strength. The framework's broader claims about constants and dimensions rest on other theorems, not on this identity alone.

What the theorem does not claim is as important as what it proves. It does not say that any particular physical system has symmetric weights; that is a modeling choice. It does not say the action is minimized or that the Laplacian has any special property; the identity holds for all fields, not just stationary ones. It does not introduce a physical source scale or fix any constant of nature. The theorem is a purely algebraic bridge between two standard forms, valuable because it is exact and general, not because it selects a preferred configuration.

/-- The Dirichlet bilinear identity:
`(1/2) ∑ᵢⱼ wᵢⱼ (eᵢ-eⱼ)(fᵢ-fⱼ) = ∑ᵢ eᵢ (Δf)ᵢ`. -/
theorem dirichlet_eq_sum_mul_laplacian
    (w : ι → ι → ℝ) (e f : ι → ℝ)
    (hsymm : ∀ i j, w i j = w j i) :
    dirichlet w e f = ∑ i, e i * laplacian w f i := by
  unfold dirichlet laplacian
  calc
    (1 / 2 : ℝ) * ∑ i, ∑ j, w i j * (e i - e j) * (f i - f j)
        = (1 / 2 : ℝ) *
            ((∑ i, ∑ j, w i j * e i * (f i - f j)) -
             (∑ i, ∑ j, w i j * e j * (f i - f j))) := by
          congr 1
          rw [← Finset.sum_sub_distrib]
          apply Finset.sum_congr rfl
          intro i _
          rw [← Finset.sum_sub_distrib]
          apply Finset.sum_congr rfl
          intro j _
          ring
    _ = ∑ i, ∑ j, w i j * e i * (f i - f j) := by
          rw [swapped_linear_term w f e hsymm]
          ring
    _ = ∑ i, e i * ∑ j, w i j * (f i - f j) := by
          apply Finset.sum_congr rfl
          intro i _
          rw [Finset.mul_sum]
          apply Finset.sum_congr rfl
          intro j _
          ring

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

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

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

What this page does not claim

No physical system is asserted to have symmetric weights; that is a modeling choice. No claim is made that the action is minimized or that the Laplacian has special properties. No physical source scale or constant of nature is fixed by this identity.

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: