Gravity Analysis Regge Hinge4 Ddihedral Kernel Partial Deficit Class Kernel Zero

The sparse deficit kernel

Regge calculus is a way of doing general relativity without a smooth manifold: spacetime is chopped into flat tetrahedra or 4-simplices, and curvature lives only along the hinges where they meet. In four dimensions, each hinge is a triangle, and the amount of curvature is measured by the deficit angle, the angle by which the surrounding simplices fail to close flat. The question is how that angle responds when you stretch one edge of the hinge while holding the flat configuration fixed.

The framework's ledger, a discrete record of geometric events, answers this question for one seed hinge inside two fixed 4-simplices. The machine-checked theorem partialDeficitClassKernel_zero_off states that the partial deficit kernel, the gradient of the deficit angle with respect to the ten squared edge lengths, is exactly zero for twelve of the fifteen edge classes. Only three classes, numbered 3, 7, and 11, carry nonzero values: negative one half, negative one half, and positive one half respectively. The result is a theorem in the framework's machine-checked library of formal theorems, with no unproved assumptions.

This sparsity is not a coincidence. The two nonzero classes pair under a symmetry that swaps two of the hinge's vertices, and the theorem also proves that the kernel is invariant under that swap. The zero classes include the uniform scaling direction, where stretching all edges together leaves the deficit angle unchanged, exactly as scale invariance demands. The nonzero classes are the directions that actually bend the hinge.

What the theorem does not do is just as precise. It does not complete the flat Hessian of the full 4D Regge action, which would require summing over every hinge in the lattice, not just the seed. It does not prove that the Regge action converges to the Einstein-Hilbert action. It does not recover the weights of that action from the deficit kernel. The full lattice orbit sum over all hinges remains open.

The practical consequence is a concrete target for further work. With the kernel's support known to be three classes, the next step is to sum this local response over the whole lattice and see whether the resulting operator matches the linearized Einstein equations. The sparsity makes that sum tractable, and the machine-checked proof makes the local piece trustworthy.

/-- THEOREM: the partial deficit kernel vanishes off classes 3, 7, 11. -/
theorem partialDeficitClassKernel_zero_off (d : Fin 15)
    (h3 : d ≠ 3) (h7 : d ≠ 7) (h11 : d ≠ 11) :
    partialDeficitClassKernel d = 0 := by
  simp only [partialDeficitClassKernel]
  rw [assembleClassKernel_eval, assembleClassKernel_eval]
  rw [show localEdgeClass 0 8 = 11 from by decide,
    show localEdgeClass 0 9 = 7 from by decide,
    show localEdgeClass 1 8 = 11 from by decide,
    show localEdgeClass 1 9 = 3 from by decide]
  rw [if_neg (show ¬((11 : Fin 15) = d) from fun h => h11 h.symm),
    if_neg (show ¬((7 : Fin 15) = d) from fun h => h7 h.symm),
    if_neg (show ¬((3 : Fin 15) = d) from fun h => h3 h.symm)]
  norm_num

/-- THEOREM: the partial deficit kernel vanishes off classes 3, 7, 11. -/
theorem partialDeficitClassKernel_zero_off (d : Fin 15)
    (h3 : d ≠ 3) (h7 : d ≠ 7) (h11 : d ≠ 11) :
    partialDeficitClassKernel d = 0 := by
  simp only [partialDeficitClassKernel]
  rw [assembleClassKernel_eval, assembleClassKernel_eval]
  rw [show localEdgeClass 0 8 = 11 from by decide,
    show localEdgeClass 0 9 = 7 from by decide,
    show localEdgeClass 1 8 = 11 from by decide,
    show localEdgeClass 1 9 = 3 from by decide]
  rw [if_neg (show ¬((11 : Fin 15) = d) from fun h => h11 h.symm),
    if_neg (show ¬((7 : Fin 15) = d) from fun h => h7 h.symm),
    if_neg (show ¬((3 : Fin 15) = d) from fun h => h3 h.symm)]
  norm_num

/-- THEOREM (symmetry): the partial deficit class kernel is invariant
under the hinge-fixing axis swap `2 ↔ 3` of the incidence layer. -/
theorem partialDeficitClassKernel_swap23 (d : Fin 15) :
    partialDeficitClassKernel (swap23Class d) =
      partialDeficitClassKernel d := by
  have hinv : ∀ x : Fin 15, swap23Class (swap23Class x) = x := by decide
  have hs3 : swap23Class 3 = 7 := by decide
  have hs7 : swap23Class 7 = 3 := by decide
  have hs11 : swap23Class 11 = 11 := by decide
  by_cases h3 : d = 3
  · subst h3
    rw [hs3, partialDeficitClassKernel_seven, partialDeficitClassKernel_three]
  by_cases h7 : d = 7
  · subst h7
    rw [hs7, partialDeficitClassKernel_three, partialDeficitClassKernel_seven]
  by_cases h11 : d = 11
  · subst h11
    rw [hs11]
  have g3 : swap23Class d ≠ 3 := fun h => h7 (by rw [← hinv d, h, hs3])
  have g7 : swap23Class d ≠ 7 := fun h => h3 (by rw [← hinv d, h, hs7])
  have g11 : swap23Class d ≠ 11 := fun h => h11 (by rw [← hinv d, h, hs11])
  rw [partialDeficitClassKernel_zero_off _ g3 g7 g11,
    partialDeficitClassKernel_zero_off _ h3 h7 h11]

What this page does not claim

The theorem does not complete the flat Hessian of the 4D Regge action. The theorem does not prove convergence to the Einstein-Hilbert action. The theorem does not recover the Einstein-Hilbert weights from the deficit kernel.

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/ReggeHinge4DDihedralKernel.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: