Gravity Regge Component Theorem3 Dproof Vertex Pair Hinge Weight Nonneg

The hinge weight

In the geometry of a triangulated three-dimensional space, a triangulation is a way of chopping a shape into tetrahedra that meet only along shared faces, edges, and vertices. A natural question is how much each edge of this mesh contributes to the space's overall curvature. The Recognition Science framework builds a number for each pair of vertices, called a hinge weight, by adding up contributions from every edge whose two endpoints are exactly that pair. Each edge's contribution is the square root of its squared length, a plain geometric quantity.

The theorem vertexPairHingeWeight_nonneg (a declaration in the framework's machine-checked library of formal theorems) proves that this hinge weight is always greater than or equal to zero. The proof is direct: it shows the weight is a sum of nonnegative terms, since a squared edge length is nonnegative and its square root is therefore nonnegative. The theorem requires only that the space has a consistent incidence geometry, meaning the edges and vertices are connected in the expected way, and that the global squared-edge chart is nonnegative. It makes no reference to any gravitational field equation or to the Regge calculus that this weight will later inform.

The importance of this result is that it separates the geometric construction from the physics. The hinge weight is defined directly from the incidence-level edge-length chart, not by negating a coefficient of the Regge Hessian matrix, which is the second derivative of the gravitational action. This independence is what the framework's ledger, its discrete record of geometric events, relies on: the weights are honest geometric data before any dynamical law is imposed. The theorem guarantees that these data stay nonnegative, a property that a later comparison with the weak-field coefficient matrix will need.

What the theorem does not claim is just as important. It does not say that the hinge weight is positive, only nonnegative; a pair of vertices with no shared edge gets a weight of exactly zero. It does not assert anything about the sign of the Regge Hessian coefficients themselves, which are a separate object. And it does not by itself establish the full comparison between the geometric weights and the weak-field matrix; that is the job of a later theorem, finalReggeComponentTarget, which builds the complete package. This small nonnegativity result is a necessary ingredient, not the whole argument.

/-- Nonnegativity of the independent incidence-defined weights, assuming the
global squared-edge chart is nonnegative. -/
theorem vertexPairHingeWeight_nonneg
    (K : Triangulation3D) (hK : IncidenceGeometry K)
    (i j : Fin K.nV) :
    0 ≤ vertexPairHingeWeight K hK i j := by
  unfold vertexPairHingeWeight edgePairIncidenceWeight
  refine Finset.sum_nonneg ?_
  intro e _
  by_cases h :
      (K.edgeVerts e).1 = i ∧ (K.edgeVerts e).2 = j ∨
        (K.edgeVerts e).1 = j ∧ (K.edgeVerts e).2 = i
  · simp [h, Real.sqrt_nonneg]
  · simp [h]

/-- Independent dual/hinge weight for a vertex pair, defined directly from
the incidence-level edge-length chart.  It is not defined by negating a
Regge Hessian coefficient. -/
def vertexPairHingeWeight
    (K : Triangulation3D) (hK : IncidenceGeometry K)
    (i j : Fin K.nV) : ℝ :=
  ∑ e : Fin K.nE, edgePairIncidenceWeight K hK i j e

What this page does not claim

The hinge weight is always positive; it can be zero for vertex pairs with no shared edge. The Regge Hessian coefficients themselves are nonnegative; this theorem concerns only the independently defined hinge weight. This theorem alone establishes the full comparison between geometric weights and the weak-field matrix.

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: