Geometry Regge Action Concrete Canonical Regge Hessian Off Diag Eq Neg Weight

The off-diagonal rule

Regge calculus is a way to do general relativity on a discrete mesh of flat tetrahedra instead of a smooth spacetime. The action, a quantity whose variation gives the equations of motion, is built from the lengths of the mesh edges and the deficit angles around them. In the framework's concrete model, a vertex potential scales each edge length by an exponential factor, and the second variation of the action defines a Hessian matrix, the discrete analogue of a second derivative.

The theorem canonicalReggeHessian_offDiag_eq_neg_weight states that for any two distinct vertices i and j of a triangulation, the Hessian entry is exactly the negative of a dual weight: H(i,j) = -w(i,j). The dual weight w(i,j) is the sum, over all edges connecting i and j, of the square root of the edge's squared length. This is a purely combinatorial and geometric identity, proved by unfolding the definition of the Hessian and simplifying.

This off-diagonal rule is the discrete counterpart of a familiar fact in continuum physics: the second derivative of an energy with respect to two different coordinates is often the negative of a coupling between them. Here it makes the Hessian a graph Laplacian: the diagonal entries sum the weights, and the off-diagonal entries subtract them. The same library proves that the Hessian is symmetric, that its rows sum to zero, and that its quadratic form is nonnegative, so the action is locally convex around the flat configuration.

In Recognition Science, the framework's account of physical structure, this theorem is one step in showing that a concrete Regge action, built from edge lengths and deficit angles, satisfies the abstract Hessian interface used elsewhere. It does not claim that this Hessian is the unique one, nor that it represents the full dynamics of general relativity. It establishes a structural identity, not a physical prediction.

theorem canonicalReggeHessian_offDiag_eq_neg_weight
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (i j : Fin K.nV) (hij : i ≠ j) :
    canonicalReggeHessian K hK i j = - canonicalDualWeight K hK i j := by
  unfold canonicalReggeHessian
  simp [hij]

theorem canonicalReggeHessian_symm
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    ∀ i j, canonicalReggeHessian K hK i j = canonicalReggeHessian K hK j i := by
  intro i j
  unfold canonicalReggeHessian
  by_cases hij : i = j
  · subst j
    rfl
  · have hji : j ≠ i := by intro h; exact hij h.symm
    simp [hij, hji, canonicalDualWeight_symm K hK i j]

theorem canonicalReggeHessian_row_sum_zero
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    ∀ i : Fin K.nV, ∑ j : Fin K.nV, canonicalReggeHessian K hK i j = 0 := by
  intro i
  unfold canonicalReggeHessian
  rw [Finset.sum_sub_distrib]
  have hdiag :
      (∑ j : Fin K.nV,
        (if i = j then ∑ k : Fin K.nV, canonicalDualWeight K hK i k else 0))
        = ∑ k : Fin K.nV, canonicalDualWeight K hK i k := by
    rw [Finset.sum_eq_single i]
    · simp
    · intro b _ hb
      have hne : i ≠ b := fun h => hb h.symm
      simp [hne]
    · intro hi
      exact (hi (Finset.mem_univ i)).elim
  rw [hdiag]
  ring

theorem canonicalReggeHessian_quadratic_nonneg
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    0 ≤ hessianQuadratic (canonicalReggeHessian K hK) ξ := by
  rw [canonicalReggeHessian_quadratic_eq_dirichlet]
  exact canonicalDirichletEnergy_nonneg K hK ξ

What this page does not claim

The theorem does not claim that this Hessian is the only possible one for a Regge action. It does not claim that the Regge action itself is derived from Recognition Science's foundational cost function. It does not claim that the discrete model reproduces the full dynamics of general relativity beyond the second-order approximation.

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: