Gravity Regge Component Theorem3 Dproof Vertex Pair Hinge Weight Symm

The symmetry of hinge weights

In the discrete geometry of Regge calculus, space is built from flat triangular or tetrahedral pieces joined along their edges, and gravity is encoded in the lengths of those edges. A key object is the hinge weight assigned to an unordered pair of vertices: a number that measures how much a given edge contributes to the geometric structure at that pair. The declaration vertexPairHingeWeight_symm establishes that this weight is symmetric, meaning the weight for the pair (i, j) equals the weight for the pair (j, i), for every pair of vertices in any triangulation.

This symmetry is not assumed; it is proved. The proof works by first showing that each individual edge's contribution to the weight is symmetric, then summing those contributions over all edges. Since a sum of symmetric terms is symmetric, the total hinge weight inherits the property. The same construction also proves the weights are nonnegative, assuming the squared edge lengths are nonnegative, which holds in any genuine geometric configuration.

In Recognition Science, this result matters because it separates the geometric data from the dynamical equations. The hinge weights are defined directly from the edge-length chart, not by negating a coefficient from the Regge Hessian matrix. The symmetry theorem guarantees that this independent geometric input is well-behaved, and it feeds into a larger comparison: the off-diagonal components of the weak-field Regge bilinear form match these weights up to sign, and the row sums satisfy the Schläfli identity. Together these facts confirm that the canonical geometric data and the dynamical equations are consistent.

The theorem does not claim that the hinge weights are derived from the Regge Hessian, nor that they are unique. It does not assert that the comparison between the geometric weights and the dynamical coefficients holds for arbitrary choices of weights; it holds for the canonical construction defined in the library. It also does not prove that the full Regge action equals the Dirichlet form for all configurations; that reduction is a separate theorem that applies once the component comparison is in hand.

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

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']

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

What this page does not claim

The hinge weights are not defined by negating a Regge Hessian coefficient. The theorem does not assert uniqueness of the hinge weights. The full equality between the Regge action and the Dirichlet form is not established by this declaration alone.

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: