Gravity Regge Component Theorem3 D

The bridge to genuine 3D Regge gravity

In lattice gravity, Regge calculus approximates spacetime by a triangulated manifold, with edge lengths as the dynamical variables. The action is built from the deficit angles around hinges, and its Hessian (the matrix of second derivatives) governs the small fluctuations. A key question is whether this discrete action, in the weak-field limit, reduces to a simple quadratic form known as the Dirichlet form, which measures the gradient energy of a scalar field. This result proves that reduction for a genuine 3D geometric computation.

The classical background: Regge calculus was introduced by Tullio Regge in 1961 as a way to do general relativity without coordinates, using a piecewise-flat simplicial complex. The Hessian of the Regge action is central to understanding linearized gravity on a lattice. The Dirichlet form, named after Peter Gustav Lejeune Dirichlet, is the standard quadratic energy functional, often written as (1/2)∫|∇φ|² dV. The theorem here shows that, under the weak-field assumption, the second-order Regge action equals (1/2) times this Dirichlet form, with the edge-area coefficients playing the role of the metric.

In Recognition Science, the framework models spacetime as a discrete ledger of recognition events, and gravity emerges from the cost structure. The library is a machine-checked collection of formal theorems. The module takes a genuine geometric component package, built from a Cayley-Menger/dihedral/Hessian computation, and shows it satisfies the existing comparison interface. This interface was previously established only for a weak-field conformal approximation; this theorem closes the gap by supplying the genuine geometric package.

The practical consequence: any computation that uses the simpler Dirichlet-form reduction can now be justified for the genuine 3D Regge Hessian, not just for a conformal approximation. This is a bridge from a formal structure to a physical computation, and it is proved in the framework's library with no unverified axioms. The theorem is a step toward showing that the discrete geometry of Regge calculus, as used in numerical relativity, is consistent with the framework's derived weak-field limit.

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

/-- A genuine component package instantiates the existing comparison
interface. -/
def componentComparison_of_genuine
    {K : Triangulation3D} (G : GenuineComponentPackage K) :
    ReggeComponentComparison G.W where
  geometricArea := G.geometricArea
  geometricArea_symm := G.geometricArea_symm
  geometricArea_nonneg := G.geometricArea_nonneg
  offDiag_component_match := G.offDiag_component_match
  schlaefli_row_sum := G.schlaefli_row_sum

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

What this page does not claim

This does not claim that the Regge action itself is derived from the framework's cost function. This does not claim that the Dirichlet-form reduction holds for strong fields or non-weak-field regimes. This does not claim that the geometric area function is the classical continuum area metric.

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: