Gravity Analysis Regge Hinge4 Ddihedral Kernel Partial Deficit Class Kernel Swap

The symmetry of the deficit kernel

In the study of gravity as a discrete geometry, one often works with a triangulated space, a space built from flat pieces glued together. The framework's library of formal theorems contains a result about a specific such construction. The declaration partialDeficitClassKernel_swap23 is a theorem that states a symmetry property of a particular mathematical object, the partial deficit class kernel. This kernel is a list of numbers, one for each of fifteen edge classes, that measures how a geometric quantity, the angle deficit, changes when the lengths of the edges in a four-dimensional simplex are varied.

The theorem itself is simple to state: swapping the labels of two specific edge classes, class 2 and class 3, leaves the kernel unchanged. In plain terms, the calculation of how the angle deficit responds to changes in edge lengths does not care whether you call a particular edge a class-2 edge or a class-3 edge. This is a symmetry of the system. The proof is a formal, machine-checked derivation, meaning it follows from the definitions and prior theorems by strict logical rules, with no gaps and no unstated assumptions. The result is not a guess or a numerical approximation; it is an exact statement about the algebraic structure of the kernel.

This symmetry is not an accident. It reflects an underlying symmetry of the geometric setup: the two edge classes in question are related by a symmetry of the seed simplex, a fundamental building block of the triangulation. The theorem confirms that the kernel respects this geometric symmetry. This is a useful check on the consistency of the construction. It also provides a non-trivial property that any complete theory of this discrete gravity model must satisfy.

It is important to be precise about what this theorem does not claim. It does not say that the full gravitational action, the quantity that describes the total energy of the geometry, is symmetric under this swap. It only concerns the partial deficit kernel, which is one component of a larger calculation. It does not prove that this kernel is the correct one for a full theory of quantum gravity. It does not say anything about the values of the kernel itself, only about its behavior under this specific relabeling. The theorem is a precise, limited, and verified statement about a single piece of a larger mathematical structure.

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

/-- 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 claim the full gravitational action is symmetric under the class 2 and 3 swap. The theorem does not claim the partial deficit kernel is the correct or complete kernel for a full theory of quantum gravity. The theorem does not claim any specific numerical value for the kernel entries.

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: