Gravity Analysis Regge Hinge4 Dflat Kernel

The 4D hinge kernel

Regge calculus is a discrete approach to general relativity where spacetime is built from flat simplexes, and gravity emerges from how the angles between them fail to sum to the flat value. In four dimensions, the fundamental object is a triangular hinge, a 2D face shared by several 4-simplexes. The module ReggeHinge4DFlatKernel establishes, with machine-checked proofs, the combinatorial scaffolding for the second variation of the Regge action around a flat configuration.

The core result is an incidence table. The module enumerates the 24 monotone 4-simplexes that tile a 4-cube, and for a specific seed triangle with vertices at 0, e0, and e0+e1, it proves that exactly two of those 24 simplexes contain it. It then counts, for each of the 15 edge classes in the stencil, how many of those two simplexes contain that class as a local edge. Three classes are proven to be absent, combinatorial decoys, while the three hinge-boundary classes each have multiplicity 2. The support is nonempty, symmetric under the axis swap 2 ↔ 3, and the total incidence sums to 20.

This is not yet the physics. The true per-hinge flat second-variation kernels, the dihedral and Cayley–Menger calculus that would supply numeric class weights, remain OPEN. The module defines a flat-Hessian assembly formula that contracts those hypothetical weights against the incidence support, but it is a MODEL, a definitional choice, not a derived result. The docstring is explicit: this does not complete the flat Hessian of the 4D Regge action, does not prove convergence to Einstein–Hilbert, and does not reverse-engineer weights from it.

What the module does establish is the combinatorial factor that any future kernel must contract against. It proves the incidence table is correct, complete, and symmetric, so that when the true deficit kernels are derived, the assembly skeleton is already in place and verified. The remaining work is a well-defined target: lift the 3D Schläfli-reduced chain to 4D, express the dihedral angle at the triangle in each incident simplex as a function of the ten squared edge lengths, differentiate at the flat point, and assemble the result into class weights.

/-- Lexicographic enumeration of the 24 permutations of `Fin 4`:
`permAxes s = (σ(0), σ(1), σ(2), σ(3))`. -/
def permAxes : Fin 24 → Fin 4 × Fin 4 × Fin 4 × Fin 4
  | 0 => (0, 1, 2, 3)
  | 1 => (0, 1, 3, 2)
  | 2 => (0, 2, 1, 3)
  | 3 => (0, 2, 3, 1)
  | 4 => (0, 3, 1, 2)
  | 5 => (0, 3, 2, 1)
  | 6 => (1, 0, 2, 3)
  | 7 => (1, 0, 3, 2)
  | 8 => (1, 2, 0, 3)
  | 9 => (1, 2, 3, 0)
  | 10 => (1, 3, 0, 2)
  | 11 => (1, 3, 2, 0)
  | 12 => (2, 0, 1, 3)
  | 13 => (2, 0, 3, 1)
  | 14 => (2, 1, 0, 3)
  | 15 => (2, 1, 3, 0)
  | 16 => (2, 3, 0, 1)
  | 17 => (2, 3, 1, 0)
  | 18 => (3, 0, 1, 2)
  | 19 => (3, 0, 2, 1)
  | 20 => (3, 1, 0, 2)
  | 21 => (3, 1, 2, 0)
  | 22 => (3, 2, 0, 1)
  | 23 => (3, 2, 1, 0)
  | ⟨n + 24, h⟩ => absurd h (by omega)

/-- THEOREM: exactly two of the 24 Freudenthal simplices contain the
seed hinge. -/
theorem seedHinge_simplex_count :
    (Finset.univ.filter (fun s : Fin 24 => containsSeedHinge s = true)).card =
      2 := by
  decide

/-- THEOREM (decoy): three explicit edge classes have zero seed-hinge
incidence. -/
theorem seedHingeIncidence_decoy_zero :
    seedHingeIncidenceNat decoyClass4 = 0 ∧
      seedHingeIncidenceNat decoyClass8 = 0 ∧
        seedHingeIncidenceNat decoyClass12 = 0 := by
  decide

/-- THEOREM (symmetry): seed-hinge incidence is invariant under the
lattice symmetry that swaps axes `2` and `3` and fixes the hinge. -/
theorem seedHingeIncidence_swap23 (d : Fin 15) :
    seedHingeIncidenceNat (swap23Class d) = seedHingeIncidenceNat d := by
  fin_cases d <;> 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 module does not complete the flat Hessian of the 4D Regge action. This module does not prove convergence of the discrete action to Einstein–Hilbert. This module does not derive the numeric weights for the per-hinge deficit kernels.

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: