Gravity Regge Component Theorem3 Dproof Genuine Component Package Of Final

The component package

Regge calculus is a discrete approach to general relativity in which spacetime is approximated by a triangulation, a network of flat simplices meeting along edges. The curvature information lives in a matrix of second derivatives of the action, and the geometric data lives in the lengths and areas of the simplices. The declaration genuine_component_package_of_final is a theorem in the framework's machine-checked library of formal theorems. It states that for any triangulation of three-dimensional space that satisfies a consistency condition on its edge lengths, there exists a package of data with two parts: a weak-field curvature matrix and a set of independent dual weights attached to vertex pairs. These weights are geometric numbers, computed directly from the edge-length chart, not defined by negating the curvature matrix.

The theorem's content is a precise component match. For any two distinct vertices i and j, the off-diagonal entry of the curvature matrix equals the negative of the dual weight for that pair. In symbols, bilinearCoefficient W i j = - dual.weight i j. The weights are symmetric and nonnegative, and the matrix satisfies a row-sum condition related to the Schläfli identity. The theorem is proved for the canonical construction: the weights come from summing the square roots of squared edge lengths over edges incident to the pair, and the curvature matrix comes from the Laplacian of those weights. The proof shows these two objects, built independently, agree component by component.

The declaration does not claim that this component match holds for arbitrary choices of weights or curvature matrices. It holds for the canonical incidence-defined construction, and the theorem is conditional on the triangulation being incidence-consistent. The theorem also does not claim that the dual weights are the same as the Regge Hessian coefficients; the whole point is that they are independent geometric data that turn out to match the off-diagonal entries. The framework's library shows that once this package exists, a Dirichlet reduction follows: the second-order Regge action equals half the Dirichlet form of the edge areas. That reduction is a separate theorem, downstream of the package construction.

What the theorem changes is the status of a geometric comparison. In Regge calculus one often assumes the dual areas are the off-diagonal curvature components; here the equality is derived from the incidence geometry rather than assumed. The machine-checked proof means the component match is not a numerical coincidence checked on examples, but a theorem for all incidence-consistent triangulations. The reader can now see that the framework's discrete gravity model has a built-in consistency between its geometric and curvature data, at least for the canonical construction.

/-- A final concrete component proof discharges `GenuineComponentPackage`. -/
theorem genuine_component_package_of_final
    (h : FinalReggeComponentTarget) :
    ∀ K : Triangulation3D, IncidenceConsistent K →
      Nonempty (GenuineComponentPackage K) := by
  intro K hK
  rcases h K hK with ⟨C⟩
  exact ⟨genuineComponentPackage_of_concrete C⟩

/-- Incidence-defined independent dual weights. -/
def independentDualWeightsOfIncidence
    (K : Triangulation3D) (hK : IncidenceGeometry K) :
    IndependentDualWeights K where
  weight := vertexPairHingeWeight K hK
  weight_symm := vertexPairHingeWeight_symm K hK
  weight_nonneg := vertexPairHingeWeight_nonneg 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

/-- Concrete component comparison built from canonical incidence weights. -/
def concreteComponentComparisonOfIncidence
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    ConcreteComponentComparison K where
  W := canonicalWeakFieldDataOfIncidence K hK
  dual := independentDualWeightsOfConsistent K hK
  offDiag_component_match := canonicalWeakFieldData_offDiag_component_match K hK
  schlaefli_row_sum := canonicalWeakFieldData_rowSum K hK

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

The theorem does not claim the component match holds for arbitrary choices of weights or curvature matrices, only for the canonical incidence-defined construction. The theorem does not claim the dual weights are the same as the Regge Hessian coefficients; they are independent geometric data that match the off-diagonal entries. The theorem does not claim any physical prediction about gravity; it is a formal statement about a discrete geometric construction.

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: