Gravity Regge Component Theorem3 D Genuine Component Package

The genuine component package

In numerical relativity, Regge calculus builds spacetime from a discrete triangulation, a mesh of tetrahedra, and writes the gravitational action as a sum over the edges of that mesh. The action's second variation, its Hessian, controls how small perturbations behave. The Recognition Science framework's machine-checked library of formal theorems contains a structure called GenuineComponentPackage that packages the data needed to connect a genuine geometric computation of this Hessian to an existing weak-field bridge.

The package, defined for a three-dimensional triangulation K, bundles five pieces of data: a weak-field Regge data set W, a geometric area function between vertices, proofs that this area function is symmetric and nonnegative, a matching condition between the bilinear coefficients of W and the geometric areas, and a row-sum property derived from Schlaefli's formula. The Schlaefli row-sum property is the key structural fact: it says that the sum of certain geometric coefficients in each row vanishes, a condition that the weak-field reduction requires.

The library proves a theorem, genuine_component_dirichlet_reduction, that applies this package: for any perturbation of the log-potential, the second-order Regge action equals one half times the Dirichlet form built from the edge areas. This is a clean identity: the complicated geometric Hessian reduces to a standard quadratic form, the Dirichlet energy, which is far easier to analyze. The theorem is proved in the machine-checked library, meaning its derivation is verified by a computer down to the axioms.

What the declaration does not claim is just as important. It does not assert that the geometric computation itself has been carried out in the library; the package is a bridge that assumes such a computation exists. It does not claim that the geometric area function is derived from the Cayley-Menger determinant or the dihedral angles; those are described as the source of the computation, but the package only records the results. And it does not claim that the Dirichlet reduction holds for all triangulations without the Schlaefli row-sum condition; that condition is an explicit hypothesis of the theorem.

/-- The genuine geometric component package produced by the
Cayley-Menger/dihedral/Hessian computation. -/
structure GenuineComponentPackage (K : Triangulation3D) where
  W : WeakFieldReggeData K.nV
  geometricArea : Fin K.nV → Fin K.nV → ℝ
  geometricArea_symm : ∀ i j, geometricArea i j = geometricArea j i
  geometricArea_nonneg : ∀ i j, 0 ≤ geometricArea i j
  offDiag_component_match :
    ∀ i j, i ≠ j → bilinearCoefficient W i j = - geometricArea i j
  schlaefli_row_sum : SchlaefliRowSum W

/-- The existing weak-field reduction applies to the genuine component
package. -/
theorem genuine_component_dirichlet_reduction
    {K : Triangulation3D} (G : GenuineComponentPackage K)
    (ε : LogPotential K.nV) :
    secondOrderReggeAction G.W ε =
      (1 / 2) * dirichletForm (edgeArea G.W) ε :=
  weak_field_conformal_reduction G.W G.schlaefli_row_sum ε

What this page does not claim

The geometric computation itself is not carried out in the library. The geometric area function is not derived from the Cayley-Menger determinant within the package. The Dirichlet reduction does not hold without the Schlaefli row-sum condition.

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/ReggeComponentTheorem3D.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: