Gravity Analysis Regge Hinge4 Ddihedral Kernel Partial Deficit Class Kernel Elev

The partial deficit kernel

In the framework's discrete model of spacetime, space is built from flat four-dimensional triangles called simplices, joined along their faces. The ledger, a discrete record of the squared lengths of every edge in this simplicial complex, determines the geometry. At a hinge, an edge shared by two simplices, the angle between the two simplices is the dihedral angle. When that angle differs from the angle in perfectly flat space, the difference is a curvature deficit, a measure of how much the local geometry bends.

The declaration partialDeficitClassKernel establishes, as a proved theorem in the machine-checked library of formal theorems, a precise statement about this curvature deficit for a specific seed configuration. The theorem, partialDeficitClassKernel_eleven, states that the partial deficit gradient, the rate at which the deficit changes as you vary the squared edge lengths, is supported on exactly three of the fifteen edge classes: classes 3, 7, and 11. For these classes, the kernel takes the values (-1/2, -1/2, +1/2); for all other classes, the kernel is zero. This means that, at the flat point, only these three particular combinations of edge lengths contribute to the first-order change in the deficit, and they do so with specific, rational weights.

This result is not an isolated computation. It is part of a chain that derives the cosine of the dihedral angle as an explicit function of the ten local squared edge lengths, proves its value is 1/√2 at the flat configuration, and computes all ten coordinate derivatives. The partial deficit kernel is then assembled from these derivatives, and the theorem partialDeficitClassKernel_swap23 shows the kernel is invariant under a symmetry that swaps two of the seed simplices' axes. The kernel is also nonvacuous: the value at class 9 is nonzero, and a uniform scaling of all lengths gives a nonzero result, while the true homothety direction gives zero exactly as scale invariance demands.

What the declaration does not claim is as important as what it proves. It does not complete the full Hessian of the 4D Regge action, the second-derivative matrix that governs the full dynamics. It does not prove that the framework's action converges to the Einstein-Hilbert action of general relativity. It does not reverse-engineer any coupling weights from the classical Einstein-Hilbert action. The result is scoped to the seed triangle hinge inside its two seed-cell Freudenthal 4-simplices only; the full lattice orbit sum over all hinges remains an open target. The theorem is a local, kernel-level statement about a specific seed configuration, not a global statement about the entire simplicial complex or its physical interpretation.

/-- 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: flat cosine squared is `1/2` (transcendental-free form). -/
theorem cosDihedral_flat_sq :
    cosDihedral seedFlatSqEdges ^ 2 = (1 / 2 : ℝ) := by
  rw [cosDihedral_flat, div_pow, one_pow,
    Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]

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

This does not complete the flat Hessian of the 4D Regge action. This does not prove S_RS_converges_EH_4d. This 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/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: