Encyclopedia Geometry Geometry Regge Action Concrete Canonical Dirichlet Equals Edge Stencil Of Sum Co

ARTICLE 3 claims 3 theorems

Geometry Regge Action Concrete Canonical Dirichlet Equals Edge Stencil Of Sum Co

In a triangulated space, the energy of a field can be written as a sum over vertices or a sum over edges; a machine-checked proof shows when these two descriptions coincide.

Verify this page

The Dirichlet energy identity

In the geometry of triangulated spaces, a Dirichlet energy measures how much a field, such as a temperature or displacement, varies across a shape. The classical definition sums squared differences over every pair of neighboring points, weighted by how strongly they are connected. A simpler, more local version sums the same squared differences only over the actual edges of the triangulation, with each edge weighted by its length. For a general weighted graph these two sums are not the same; the vertex version can count a connection twice or miss it entirely unless the weights obey special symmetries.

The theorem canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex in the framework's machine-checked library of formal theorems establishes exactly when they do agree. It proves that for any incidence-consistent three-dimensional triangulation, if two technical conditions hold, then the canonical Dirichlet energy over vertex pairs equals the edge-stencil Dirichlet energy over edges. The first condition, CanonicalEdgeStencilSumCommTarget, requires that summing a squared edge difference over all ordered vertex pairs gives twice the contribution of that edge alone. The second, CanonicalEdgePairWeightReindexTarget, requires that reindexing the double sum over vertices reproduces the same weighted edge term. Together they guarantee that the vertex-pair sum collapses cleanly onto the edge sum, with no double counting and no missing terms.

The proof itself is a formal derivation in the framework's library: it takes the two stated hypotheses and rewrites the vertex-pair sum by reindexing and commutativity until it matches the edge-stencil expression. The declaration is a theorem, not a definition, so it is a proved statement about the framework's own ledger, its discrete record of geometric data. Its role is to connect two ways of writing the same quadratic form, a step used in showing that the second variation of the Regge action, a discrete version of general relativity's action, has the expected Hessian structure.

What the theorem does not claim is just as important. It does not assert that the two conditions hold for every triangulation; they are hypotheses, and the theorem only says that if they hold, the equality follows. It does not prove that the edge-stencil energy is the physically correct one, only that it coincides with the vertex-pair version under the stated assumptions. And it says nothing about the Regge action itself, only about the quadratic form that appears in its second-order expansion. The equality is a tool, not a physical law.

For a reader meeting this result fresh, the practical consequence is that two apparently different sums, one over vertex pairs and one over edges, are interchangeable in the framework's geometry whenever the two reindexing conditions are satisfied. That interchange is what lets later steps in the library treat the Hessian of the Regge action as a Dirichlet energy, opening the way to spectral and positivity arguments. The identity is a bridge between two notations, and the theorem certifies that the bridge holds.

THEOREM canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex · IndisputableMonolith/Geometry/ReggeActionConcrete.lean
canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex · IndisputableMonolith/Geometry/ReggeActionConcrete.lean:561 
theorem canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hSum : CanonicalEdgeStencilSumCommTarget K hK)
    (hReindex : CanonicalEdgePairWeightReindexTarget K hK) :
    CanonicalDirichletEqualsEdgeStencilTarget K hK := by
  intro ξ
  unfold canonicalDirichletEnergy canonicalEdgeStencilDirichletEnergy canonicalDualWeight
  rw [hSum ξ]
  calc
    (1 / 2) * (∑ e : Fin K.nE, ∑ i : Fin K.nV, ∑ j : Fin K.nV,
      canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ))
        = ∑ e : Fin K.nE, (1 / 2) * (∑ i : Fin K.nV, ∑ j : Fin K.nV,
            canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)) := by
            rw [Finset.mul_sum]
    _ = ∑ e : Fin K.nE,
        Real.sqrt (hK.globalSqEdge e) *
          (ξ (K.edgeVerts e).1 - ξ (K.edgeVerts e).2) ^ (2 : ℕ) := by
        refine Finset.sum_congr rfl ?_
        intro e _
        rw [hReindex ξ e]
        ring
THEOREM canonicalEdgeStencilSumComm · IndisputableMonolith/Geometry/ReggeActionConcrete.lean
canonicalEdgeStencilSumComm · IndisputableMonolith/Geometry/ReggeActionConcrete.lean:536 
theorem canonicalEdgeStencilSumComm
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    CanonicalEdgeStencilSumCommTarget K hK := by
  intro ξ
  simp_rw [Finset.sum_mul]
  calc
    (∑ i : Fin K.nV, ∑ j : Fin K.nV, ∑ e : Fin K.nE,
      canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ))
        = ∑ i : Fin K.nV, ∑ e : Fin K.nE, ∑ j : Fin K.nV,
            canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ) := by
            refine Finset.sum_congr rfl ?_
            intro i _
            exact (Finset.sum_comm :
              (∑ j : Fin K.nV, ∑ e : Fin K.nE,
                canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)) =
              (∑ e : Fin K.nE, ∑ j : Fin K.nV,
                canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)))
    _ = ∑ e : Fin K.nE, ∑ i : Fin K.nV, ∑ j : Fin K.nV,
            canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ) := by
            exact (Finset.sum_comm :
              (∑ i : Fin K.nV, ∑ e : Fin K.nE, ∑ j : Fin K.nV,
                canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)) =
              (∑ e : Fin K.nE, ∑ i : Fin K.nV, ∑ j : Fin K.nV,
                canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)))
THEOREM canonicalEdgePairWeightReindex_of_noSelfLoop · IndisputableMonolith/Geometry/ReggeActionConcrete.lean
canonicalEdgePairWeightReindex_of_noSelfLoop · IndisputableMonolith/Geometry/ReggeActionConcrete.lean:428 
theorem canonicalEdgePairWeightReindex_of_noSelfLoop
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hNoLoop : NoSelfLoopEdges K) :
    CanonicalEdgePairWeightReindexTarget K hK := by
  intro ξ e
  let a := (K.edgeVerts e).1
  let b := (K.edgeVerts e).2
  let inner := fun i : Fin K.nV =>
    ∑ j : Fin K.nV,
      canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ)
  have hab : a ≠ b := hNoLoop e
  have hinner_a : inner a =
      Real.sqrt (hK.globalSqEdge e) * (ξ a - ξ b) ^ (2 : ℕ) := by
    unfold inner
    rw [Finset.sum_eq_single b]
    · simp [canonicalEdgePairWeight, a, b, hab]
    · intro j _ hjb
      have hnot1 : ¬ ((K.edgeVerts e).1 = a ∧ (K.edgeVerts e).2 = j) := by
        intro h
        exact hjb (by simpa [b] using h.2.symm)
      have hnot2 : ¬ ((K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = a) := by
        intro h
        have hba : b = a := by simpa [b] using h.2
        exact hab hba.symm
      simp [canonicalEdgePairWeight, hnot1, hnot2]
    · intro hb
      exact (hb (Finset.mem_univ b)).elim
  have hinner_b : inner b =
      Real.sqrt (hK.globalSqEdge e) * (ξ b - ξ a) ^ (2 : ℕ) := by
    unfold inner
    rw [Finset.sum_eq_single a]
    · have hba : b ≠ a := fun h => hab h.symm
      simp [canonicalEdgePairWeight, a, b, hab, hba]
    · intro j _ hja
      have hnot1 : ¬ ((K.edgeVerts e).1 = b ∧ (K.edgeVerts e).2 = j) := by
        intro h
        have hab' : a = b := by simpa [a] using h.1
        exact hab hab'
      have hnot2 : ¬ ((K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = b) := by
        intro h
        exact hja (by simpa [a] using h.1.symm)
      simp [canonicalEdgePairWeight, hnot1, hnot2]
    · intro ha
      exact (ha (Finset.mem_univ a)).elim
  have hinner_other : ∀ i : Fin K.nV, i ≠ a → i ≠ b → inner i = 0 := by
    intro i hia hib
    unfold inner
    refine Finset.sum_eq_zero ?_
    intro j _
    have hnot1 : ¬ ((K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j) := by
      intro h
      exact hia (by simpa [a] using h.1.symm)
    have hnot2 : ¬ ((K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i) := by
      intro h
      exact hib (by simpa [b] using h.2.symm)
    simp [canonicalEdgePairWeight, hnot1, hnot2]
  have hb_mem : b ∈ (Finset.univ : Finset (Fin K.nV)) \ {a} := by
    simp [hab.symm]
  calc
    (∑ i : Fin K.nV, ∑ j : Fin K.nV,
      canonicalEdgePairWeight K hK i j e * (ξ i - ξ j) ^ (2 : ℕ))
        = ∑ i : Fin K.nV, inner i := rfl
    _ = inner a + ∑ i ∈ (Finset.univ : Finset (Fin K.nV)) \ {a}, inner i := by
      exact Finset.sum_eq_add_sum_diff_singleton
        (s := (Finset.univ : Finset (Fin K.nV))) (i := a)
        (h := Finset.mem_univ a) (f := inner)
    _ = inner a + (inner b + ∑ i ∈ ((Finset.univ : Finset (Fin K.nV)) \ {a}) \ {b}, inner i) := by
      congr 1
      exact Finset.sum_eq_add_sum_diff_singleton
        (s := ((Finset.univ : Finset (Fin K.nV)) \ {a})) (i := b)
        (h := hb_mem) (f := inner)
    _ = inner a + inner b := by
      have hzero :
          (∑ i ∈ ((Finset.univ : Finset (Fin K.nV)) \ {a}) \ {b}, inner i) = 0 := by
        refine Finset.sum_eq_zero ?_
        intro i hi
        have hia : i ≠ a := by
          intro h
          subst i
          simp at hi
        have hib : i ≠ b := by
          intro h
          subst i
          simp at hi
        exact hinner_other i hia hib
      rw [hzero]
      ring
    _ = Real.sqrt (hK.globalSqEdge e) * (ξ a - ξ b) ^ (2 : ℕ) +
        Real.sqrt (hK.globalSqEdge e) * (ξ b - ξ a) ^ (2 : ℕ) := by
      rw [hinner_a, hinner_b]
    _ = 2 * Real.sqrt (hK.globalSqEdge e) *
        (ξ (K.edgeVerts e).1 - ξ (K.edgeVerts e).2) ^ (2 : ℕ) := by
      have hsq : (ξ b - ξ a) ^ (2 : ℕ) = (ξ a - ξ b) ^ (2 : ℕ) := by ring
      rw [hsq]
      simp [a, b]
      ring

What this page does not claim

The theorem does not prove that the two reindexing conditions hold for any particular triangulation; they are hypotheses. The theorem does not identify the edge-stencil energy as the physically correct energy; it only proves equality under the stated assumptions. The theorem does not make any claim about the Regge action itself, only about the quadratic form in its second-order expansion.

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/Geometry/ReggeActionConcrete.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND