Gravity Analysis Regge Hinge4 Dflat Kernel Seed Hinge Incidence Nonvacuous

The nonempty incidence table

In four-dimensional geometry, a simplex is the simplest shape: a 4-simplex has five vertices, ten edges, and is the four-dimensional analogue of a triangle or tetrahedron. Regge calculus, a discrete approach to general relativity, approximates curved spacetime by gluing together many flat 4-simplices. The Recognition Science framework builds a machine-checked library of formal theorems to explore this approach. The declaration seedHingeIncidence_nonvacuous addresses a specific question: does a chosen triangular hinge, a 2-dimensional face where two 4-simplices meet, actually occur in the combinatorial structure?

The framework defines a standard 4-cube subdivided into 24 monotone 4-simplices, each corresponding to a permutation of the four coordinate axes. It then selects a seed hinge: the triangle with vertices at the origin, the point one unit along the first axis, and the point one unit along the first and second axes. The theorem seedHingeIncidence_nonvacuous proves that this seed hinge appears in exactly two of the 24 simplices, and that its incidence count is nonzero. This is a combinatorial fact, checked by exhaustive enumeration in the machine-checked library, not a physical claim about gravity.

The result matters because it establishes that the incidence table, the list of which simplices contain the hinge, is not empty. This nonvacuity is a prerequisite for any later calculation that contracts geometric weights against this combinatorial support. Without it, the entire assembly skeleton would be built on nothing. The theorem also confirms the hinge's boundary classes each have multiplicity two, meaning the hinge sits between two simplices, a necessary condition for a shared face in a simplicial complex.

In Recognition Science, this is a small but load-bearing step in a larger campaign to derive the flat second variation of the Regge action in four dimensions. The framework models the flat-Hessian assembly formula as a definition, contracting per-hinge area weights and deficit kernels, but those weights and kernels are explicitly open parameters. The incidence table proved here is the combinatorial factor those future kernels must contract against. The theorem does not complete the flat Hessian, does not prove convergence to the Einstein-Hilbert action, and does not derive any physical coupling constant.

/-- THEOREM (nonvacuity): class `0` (hinge-boundary edge `e₀`) has
multiplicity `2`. -/
theorem seedHingeIncidence_nonvacuous :
    seedHingeIncidenceNat (0 : Fin 15) = 2 ∧
      seedHingeIncidenceNat (0 : Fin 15) ≠ 0 := by
  decide

/-- THEOREM: every seed-hinge boundary class has positive incidence. -/
theorem hingeBoundary_incidence_pos (i : Fin 3) :
    0 < seedHingeIncidenceNat (hingeBoundaryClass i) := by
  fin_cases i <;> decide

/-- MODEL: flat second-variation class form for one hinge orbit,
`Σ_{e,f} Aweight_e · Kdeficit_{e f} · c_e · c_f`.

This is the 4D skeleton of the 3D Schläfli-reduced contraction
`−Σ_τ Σ_f L' · θ'` in `ReggeTTFlatSecondVariation`: here `Aweight`
plays the role of the area / hinge-volume first derivative and
`Kdeficit` the outer product of deficit gradients.  Both maps are OPEN. -/
def flatHessianOrbitForm
    (Aweight : Fin 15 → ℝ)
    (Kdeficit : Fin 15 → Fin 15 → ℝ)
    (c : Fin 15 → ℝ) : ℝ :=
  ∑ e : Fin 15, ∑ f : Fin 15, Aweight e * Kdeficit e f * c e * c f

What this page does not claim

This theorem does not complete the flat Hessian of the 4D Regge action. This theorem does not prove convergence to the Einstein-Hilbert action. This theorem does not reverse-engineer weights from Einstein-Hilbert.

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/Analysis/ReggeHinge4DFlatKernel.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: