Encyclopedia Geometry Geometry Regge Action Concrete Canonical Edge Pair Weight Reindex Of No Self Loo

ARTICLE 3 claims 3 theorems

Geometry Regge Action Concrete Canonical Edge Pair Weight Reindex Of No Self Loo

A machine-checked lemma shows that a certain sum over vertex pairs collapses to a single edge term, but only when the triangulation has no self-loops.

Verify this page

The edge reindexing lemma

In a finite three-dimensional triangulation, the Regge action is a discrete model of general relativity built from tetrahedra. The framework's machine-checked library of formal theorems works with a concrete version of this action. The declaration canonicalEdgePairWeightReindex_of_noSelfLoop proves a technical identity about how a sum over all ordered pairs of vertices can be re-expressed as a sum over edges.

The identity concerns a weight function defined on pairs of vertices and an edge. For a fixed edge with endpoints u and v, the weight is the square root of the squared edge length if the pair is exactly (u,v) or (v,u), and zero otherwise. The theorem states that summing this weight times the squared difference of a vertex potential over all ordered pairs (i,j) equals twice the square root of the squared edge length times the squared difference of the potential at the two endpoints. This is a reindexing result: it shows that the double sum over vertices collapses to a single term per edge.

The theorem requires the hypothesis NoSelfLoopEdges, which asserts that no edge has the same vertex at both ends. This condition is necessary because the weight function treats the two endpoints of an edge as distinct; if an edge were a self-loop, the ordered pair (u,u) would not match the pattern (u,v) with u ≠ v, and the identity would fail. The proof proceeds by unfolding the definition of the weight and applying the no-self-loop condition to rule out the degenerate case.

This lemma is a stepping stone, not a final result. It feeds into the larger theorem canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex, which combines this reindexing with a separate commutation result to show that a canonical Dirichlet energy equals an edge-stencil energy. That equality, in turn, supports the positivity of the Hessian quadratic form, a key property for stability analysis of the Regge action.

What the declaration does not claim is just as important. It does not assert that the Regge action is physically correct, that the triangulation is non-degenerate, or that the vertex potential satisfies any equation of motion. It only establishes a combinatorial identity under the stated no-self-loop condition. The theorem is a formal statement in the library; its application to physics is a separate step.

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
THEOREM NoSelfLoopEdges · IndisputableMonolith/Geometry/ReggeActionConcrete.lean
NoSelfLoopEdges · IndisputableMonolith/Geometry/ReggeActionConcrete.lean:425 
def NoSelfLoopEdges (K : Triangulation3D) : Prop :=
  ∀ e : Fin K.nE, (K.edgeVerts e).1 ≠ (K.edgeVerts e).2
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

What this page does not claim

The Regge action is a physically correct model of general relativity. The triangulation is non-degenerate or satisfies any geometric regularity condition. The vertex potential satisfies any equation of motion or variational principle.

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