Gravity Regge Component Theorem3 Dproof Edge Pair Incidence Weight Symm

The symmetry of edge weights

In the geometry of a triangulated three-dimensional space, a triangulation is a way of filling a volume with tetrahedra that meet only along shared faces, edges, or vertices. A central object of study is the Regge action, a discrete version of the Einstein-Hilbert action of general relativity, built from the edge lengths of the triangulation. The declaration edgePairIncidenceWeight_symm is a theorem in the framework's machine-checked library of formal theorems. It states that for any triangulation, any two vertices i and j, and any edge e, the weight assigned to the unordered pair (i, j) equals the weight assigned to (j, i). In plain language, the order in which you name the two endpoints of an edge does not matter; the geometric data attached to the pair is symmetric.

This symmetry is not an assumption. The library proves it from the definition of the weight itself. The weight of an edge for a vertex pair is the square root of the global squared edge length if the edge's endpoints are exactly those two vertices, and zero otherwise. Since the condition checks whether the endpoints are (i, j) or (j, i), the two cases are logically identical, and the theorem follows by case analysis. The same symmetry then extends to the sum over all edges, giving the vertex-pair hinge weight, and from there to the construction of independent dual weights for the whole triangulation. The library also proves these weights are nonnegative, assuming the squared-edge chart is nonnegative.

In Recognition Science, this symmetry is a load-bearing step in a larger program. The framework models gravity on a discrete triangulation using a ledger, a discrete record of geometric events, and derives the Regge action from a forced cost function. The theorem here is part of a chain that separates the independent geometric data, the dual weights, from the weak-field coefficient matrix. The final target, finalReggeComponentTarget, is a theorem that for any incidence-consistent triangulation, the off-diagonal components of the weak-field bilinear form equal the negative of the dual weight, and the row sums satisfy the Schläfli identity. The symmetry theorem is the first step that makes this comparison well-defined, because a comparison between two objects requires both to treat vertex pairs in the same order-independent way.

What the theorem does not claim is equally important. It does not assert that the weights are derived from the Regge Hessian; in fact, the pack explicitly separates these independent dual weights as geometric data, not defined by negating the Regge coefficient matrix. It does not claim that the Regge action itself is symmetric in any stronger sense, nor that the full physical content of general relativity is captured by this discrete model. The theorem is a precise, narrow statement about the order-independence of a geometric weight, and its value lies in the fact that it is proved, not assumed, within a machine-checked formal system.

theorem edgePairIncidenceWeight_symm
    (K : Triangulation3D) (hK : IncidenceGeometry K)
    (i j : Fin K.nV) (e : Fin K.nE) :
    edgePairIncidenceWeight K hK i j e =
      edgePairIncidenceWeight K hK j i e := by
  unfold edgePairIncidenceWeight
  by_cases h :
      (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j ∨
        (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i
  · have h' :
        (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i ∨
          (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j := by
      exact h.symm
    simp [h, h']
  · have h' :
        ¬ ((K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i ∨
          (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j) := by
      intro hx
      exact h hx.symm
    simp [h, h']

theorem vertexPairHingeWeight_symm
    (K : Triangulation3D) (hK : IncidenceGeometry K)
    (i j : Fin K.nV) :
    vertexPairHingeWeight K hK i j = vertexPairHingeWeight K hK j i := by
  unfold vertexPairHingeWeight
  refine Finset.sum_congr rfl ?_
  intro e _
  exact edgePairIncidenceWeight_symm K hK i j e

/-- Nonnegativity of the independent incidence-defined weights, assuming the
global squared-edge chart is nonnegative. -/
theorem vertexPairHingeWeight_nonneg
    (K : Triangulation3D) (hK : IncidenceGeometry K)
    (i j : Fin K.nV) :
    0 ≤ vertexPairHingeWeight K hK i j := by
  unfold vertexPairHingeWeight edgePairIncidenceWeight
  refine Finset.sum_nonneg ?_
  intro e _
  by_cases h :
      (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j ∨
        (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i
  · simp [h, Real.sqrt_nonneg]
  · simp [h]

/-- The arbitrary-triangulation component target is discharged for the
canonical incidence/Laplacian second-order Regge data. -/
theorem finalReggeComponentTarget : FinalReggeComponentTarget := by
  intro K hK
  exact ⟨concreteComponentComparisonOfIncidence K hK⟩

What this page does not claim

The theorem does not claim that the dual weights are derived from the Regge Hessian; they are independent geometric data. It does not claim that the Regge action is symmetric in any stronger sense than the order-independence of vertex-pair weights. It does not claim that the full physical content of general relativity is captured by this discrete model.

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/Gravity/ReggeComponentTheorem3DProof.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: