Gravity Regge Component Theorem3 D Genuine Component Dirichlet Reduction

The geometric bridge

In numerical relativity and lattice gauge theory, the Regge calculus is a way to discretize spacetime: instead of a smooth manifold, one works with a triangulated space, where the geometry is encoded in the edge lengths of simplices. The action, which governs the dynamics, is a sum over hinges (in 3D, the edges) of the deficit angle times the hinge area. The second-order variation of this action, the Hessian, is what appears in linearized analyses and in the study of small fluctuations around a background.

The declaration genuine_component_dirichlet_reduction is a theorem in the framework's machine-checked library of formal theorems. It states that for a triangulated 3D manifold, given a genuine geometric component package (which supplies the geometric areas and the bilinear coefficients of the Hessian), the second-order Regge action equals one half times the Dirichlet form built from the edge areas. In symbols, the theorem reads: secondOrderReggeAction G.W ε = (1/2) * dirichletForm (edgeArea G.W) ε. This is not a numerical approximation; it is an exact identity, proved in the Lean 4 proof assistant with no axioms beyond the standard three.

The content of the theorem is a bridge. The geometric computation, which comes from the Cayley-Menger determinant and dihedral angles, produces a package that satisfies the interface of an earlier, weak-field conformal Regge bridge. The theorem then applies the previously proved reduction to this genuine package. The upshot is that the complicated-looking second-order action, which involves the Hessian of the Regge action, collapses to a much simpler quadratic form, the Dirichlet form, which is a standard object in analysis and potential theory. This is a structural simplification: it says that, at second order, the discrete gravity action behaves like a simple harmonic system with the edge areas playing the role of the metric in the energy functional.

In Recognition Science, this theorem is one step in a larger program of deriving physical structure from a ledger of recognition events. The framework models spacetime as a discrete structure, and this theorem is part of the machinery that connects the discrete geometry to continuum-like field theory. The Dirichlet form is a natural object in this context because it is the quadratic form associated with the Laplacian, and it appears here as the effective second-order action.

What the theorem does not claim is equally important. It does not claim that the full, non-linear Regge action is equal to a Dirichlet form; the identity holds only at second order, for the quadratic part of the action. It does not claim that the Dirichlet form is the full dynamics; it is the second-order approximation. And it does not claim that the geometric component package exists for every triangulation; the theorem takes such a package as a hypothesis. The theorem is a conditional statement: if you have a genuine geometric component package, then the reduction holds.

/-- 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 full non-linear Regge action equals a Dirichlet form. The Dirichlet form captures the complete dynamics, not just the second-order approximation. A genuine geometric component package exists for every triangulation.

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: