Foundation Pair Kernel Source Variation Action Eq Dirichlet Self

The energy identity

A quadratic form is one of the most common objects in physics and mathematics: it takes a vector and returns a number by summing products of its components. The declaration action_eq_dirichlet_self concerns a specific quadratic form built from a finite set of points, a symmetric weight between each pair, and a real number at each point. It states that the action, defined as half the sum over all ordered pairs of the weight times the squared difference of the field values, is identical to the Dirichlet form evaluated on the same field. The Dirichlet form here is the polarized version: half the sum over ordered pairs of the weight times the product of the two differences. Setting the second field equal to the first reduces the product to a square, which is exactly the action. The theorem is proved in the framework's machine-checked library of formal theorems.

The identity is not a physical law; it is a mathematical tautology that holds for any symmetric weight matrix and any real-valued field on a finite index set. Its content is algebraic: the quadratic action can be rewritten as a sum of products involving the graph Laplacian, which is defined as the sum over j of the weight times the field difference. The theorem action_eq_sum_mul_laplacian, which follows directly, states that the action equals the sum over i of the field at i times the Laplacian at i. This is the discrete analogue of the classical integration-by-parts identity that relates a gradient energy to a Laplacian acting on the field. The coefficient 2 in the first variation along a line, derived in the same file, is a consequence of the quadratic structure and the symmetry of the weights.

In Recognition Science, this identity is a bridge between the framework's ledger, a discrete record of events with pairwise weights, and the standard language of variational calculus. The framework models a source as a field on a finite set and an action as a quadratic cost of recognition. The theorem shows that this cost can be expressed in two equivalent ways: directly as a sum of squared differences, or as a pairing of the field with its Laplacian. Both forms are useful for different purposes, and the identity guarantees they are interchangeable. The proof requires no new axioms and contains no gaps; it is a fully verified statement within the framework's formal system.

What the declaration does not claim is equally important. It does not assert that the action is physically meaningful or that the weights correspond to any actual interaction. The action is a mathematical model input, as the file's documentation states. The identity does not select an additional physical source scale; it is purely structural. It does not imply that the Laplacian has any particular spectral property, nor that the field satisfies any equation of motion. The theorem is about the equivalence of two algebraic expressions, not about the dynamics of a physical system. A reader who takes the identity as a definitional convenience is correct; a reader who reads into it a physical principle would be overinterpreting.

/-- The quadratic action is the Dirichlet form on the diagonal. -/
theorem action_eq_dirichlet_self (w : ι → ι → ℝ) (e : ι → ℝ) :
    action w e = dirichlet w e e := by
  unfold action dirichlet
  congr 1
  apply Finset.sum_congr rfl
  intro i _
  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 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 identity does not assert that the action is physically meaningful or that the weights correspond to any actual interaction. The declaration does not select an additional physical source scale. The theorem does not imply that the field satisfies any equation of motion.

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: