Foundation Pair Kernel Source Variation Action Has Deriv At Line Laplacian

The derivative of the action

The declaration concerns a mathematical object called a quadratic form, a rule that assigns a number to a collection of values. In the framework's model, the values sit at the vertices of a finite graph, and the rule is a weighted sum of squared differences between neighboring values. The specific form here is action, a ledger entry that records the total cost of a configuration as half the sum over all pairs of a weight times the square of the value difference.

The statement shows how that action changes when every value is shifted along a straight line. If you add a small multiple of a direction vector to the base configuration, the action changes at a rate exactly equal to twice a certain bilinear expression, the Dirichlet form. The derivative at zero is not an approximation; it is an exact algebraic identity that holds for any finite graph, any symmetric weights, and any real direction vector.

The same derivative can be written using the graph Laplacian, a linear operator that measures how a value at a vertex differs from its neighbors. In that form, the rate of change is twice the sum over vertices of the direction value times the Laplacian of the base configuration. This is the statement of action_hasDerivAt_line_laplacian: the derivative of the action along a line equals that Laplacian-weighted sum, provided the weights are symmetric.

The reasoning is a short chain of identities. The action equals its own Dirichlet form on the diagonal, the Dirichlet form obeys a bilinear identity with the Laplacian, and the line expansion of the action is exact. No limits are needed because the expression is polynomial in the line parameter. The library's statement records the result with no unproved assumptions beyond the symmetry of the weights.

In Recognition Science, this result is a tool, not a law of nature. The action is a mathematical model input; the statement does not select a physical source scale, does not derive any constant, and does not say which graph or weights to use. It is a clean statement about the geometry of a finite quadratic form, useful for later steps but carrying no empirical content by itself.

/-- In Laplacian form, the exact first variation is
`2 * ∑ᵢ vᵢ (Δe)ᵢ`. -/
theorem action_hasDerivAt_line_laplacian
    (w : ι → ι → ℝ) (e v : ι → ℝ)
    (hsymm : ∀ i j, w i j = w j i) :
    HasDerivAt
      (fun t : ℝ => action w (fun i => e i + t * v i))
      (2 * ∑ i, v i * laplacian w e i)
      0 := by
  rw [← dirichlet_eq_sum_mul_laplacian_swapped w e v hsymm]
  exact action_hasDerivAt_line w e v

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

/-- The bilinear identity with the variation in the Laplacian slot. -/
theorem dirichlet_eq_sum_mul_laplacian_swapped
    (w : ι → ι → ℝ) (e f : ι → ℝ)
    (hsymm : ∀ i j, w i j = w j i) :
    dirichlet w e f = ∑ i, f i * laplacian w e i := by
  calc
    dirichlet w e f = dirichlet w f e := by
      unfold dirichlet
      congr 1
      apply Finset.sum_congr rfl
      intro i _
      apply Finset.sum_congr rfl
      intro j _
      ring
    _ = ∑ i, f i * laplacian w e i :=
      dirichlet_eq_sum_mul_laplacian w f 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 statement does not select a physical source scale or derive any constant. The statement does not say which graph or weights to use for a physical system. The statement does not require differentiability assumptions; it is an exact algebraic 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: