Gravity Regge Component Theorem3 Dproof

The component theorem

Regge calculus is a discrete approach to general relativity in which spacetime is chopped into flat tetrahedral pieces, and gravity is described by how the edge lengths of those pieces deviate from a flat geometry. The ledger, a discrete record of geometric events, keeps track of these edge lengths. The central object is the Regge action, a sum over the mesh that measures total curvature, and its second derivative, the Hessian, gives the weak-field force coefficients between pairs of vertices.

The module ReggeComponentTheorem3DProof establishes that these force coefficients can be computed independently, directly from the geometry of the mesh, rather than by differentiating the action. It defines a dual weight for each pair of vertices: the square root of the squared edge length, summed over all edges connecting that pair. This weight is symmetric and nonnegative, and it is built purely from the incidence structure of the triangulation, meaning from which vertices are connected by which edges.

The main theorem, finalReggeComponentTarget, proves that for any consistent triangulation, this independently computed weight equals the negative of the off-diagonal coefficient of the Regge Hessian. In symbols, for distinct vertices i and j, the bilinear coefficient of the weak-field data equals minus the dual weight. This is the component-wise match that the theorem name promises. The proof also verifies that the row sums of the coefficient matrix vanish, a property known as the Schläfli row sum, which is required for the action to be invariant under uniform scaling.

In Recognition Science, this result matters because it separates the geometric content of gravity from the dynamical equations. The dual weights are not defined by negating a Hessian coefficient; they are independent geometric data. The theorem shows that the weak-field Regge action, when built from these weights, reproduces the genuine Regge Hessian component by component. This is a structural consistency check: the force law between vertices is exactly what the geometry dictates, with no free parameters.

The practical consequence is a reduction. Once the component match is established, the second-order Regge action reduces to a Dirichlet form, a standard quadratic energy, on the logarithms of edge lengths. This reduction is the bridge from the discrete action to a solvable linear system, and it is what makes the weak-field limit of Regge calculus tractable for further analysis.

/-- The arbitrary-triangulation component target is discharged for the
canonical incidence/Laplacian second-order Regge data. -/
theorem finalReggeComponentTarget : FinalReggeComponentTarget := by
  intro K hK
  exact ⟨concreteComponentComparisonOfIncidence K hK⟩

theorem canonicalWeakFieldData_offDiag_component_match
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (i j : Fin K.nV) (hij : i ≠ j) :
    bilinearCoefficient (canonicalWeakFieldDataOfIncidence K hK) i j =
      - (independentDualWeightsOfConsistent K hK).weight i j := by
  rw [canonicalWeakFieldData_bilinearCoefficient]
  exact Geometry.ReggeActionConcrete.canonicalReggeHessian_offDiag_eq_neg_weight K hK i j hij

theorem canonicalWeakFieldData_rowSum
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    SchlaefliRowSum (canonicalWeakFieldDataOfIncidence K hK) :=
  schlaefliRowSum_laplacianReggeData
    (Geometry.ReggeActionConcrete.canonicalDualWeight K hK)
    (Geometry.ReggeActionConcrete.canonicalDualWeight_symm K hK)

/-- Independent dual weights attached to vertex pairs of a triangulation.
These are geometric data, not defined by negating the Regge coefficient
matrix. -/
structure IndependentDualWeights (K : Triangulation3D) where
  weight : Fin K.nV → Fin K.nV → ℝ
  weight_symm : ∀ i j, weight i j = weight j i
  weight_nonneg : ∀ i j, 0 ≤ weight i j

/-- Once the final component package is constructed, the existing Dirichlet
reduction applies immediately. -/
theorem genuine_component_dirichlet_reduction_from_final
    {K : Triangulation3D} (C : ConcreteComponentComparison K)
    (ε : LogPotential K.nV) :
    secondOrderReggeAction C.W ε =
      (1 / 2) * dirichletForm (edgeArea C.W) ε :=
  genuine_component_dirichlet_reduction (genuineComponentPackage_of_concrete C) ε

What this page does not claim

This module does not prove that Regge calculus converges to general relativity in the continuum limit. This module does not derive the Einstein field equations from the Regge action. This module does not establish uniqueness of the dual weight construction; other geometric weights may also satisfy the component match.

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: