Gravity Analysis Regge Hinge4 Dstar Kernel Full Star Class Kernel Swap23

The swap symmetry

The declaration fullStarClassKernel_swap23 is a machine-checked theorem in the framework's library of formal mathematics. It concerns a specific construction in four-dimensional geometry: a lattice of points, a seed triangle, and the six four-dimensional simplices that contain it. The theorem states that if you swap two of the coordinate directions, the numerical value assigned to each of the fifteen symmetry classes of the construction remains exactly the same. In plain terms, the computed curvature contribution does not care which of those two directions you call first.

This is a symmetry property, not a physical law. The framework models gravity on a discrete lattice, where space is built from flat triangular pieces meeting along edges. The declaration is one step in a larger campaign to show that this discrete model reproduces the Einstein–Hilbert action of general relativity in the right limit. The swap symmetry is a consistency check: the model's answer should not depend on an arbitrary labeling of coordinates. The theorem is proved by direct computation over the finite set of fifteen classes, with no gaps in the proof.

The declaration does not claim that the full model converges to Einstein–Hilbert gravity. That remains an open target. It does not claim to have assembled the complete flat Hessian over all hinges, nor to have derived the weights of the model from general relativity. The swap symmetry is one verified property of one part of the construction, not the whole story.

theorem fullStarClassKernel_swap23 (d : Fin 15) :
    fullStarClassKernel (swap23Class d) = fullStarClassKernel d := by
  have hinv : ∀ x : Fin 15, swap23Class (swap23Class x) = x := by decide
  have hs2 : swap23Class (2 : Fin 15) = 2 := by decide
  have hs3 : swap23Class (3 : Fin 15) = 7 := by decide
  have hs6 : swap23Class (6 : Fin 15) = 10 := by decide
  have hs7 : swap23Class (7 : Fin 15) = 3 := by decide
  have hs10 : swap23Class (10 : Fin 15) = 6 := by decide
  have hs11 : swap23Class (11 : Fin 15) = 11 := by decide
  have hs14 : swap23Class (14 : Fin 15) = 14 := by decide
  by_cases h2 : d = 2
  · subst h2; rw [hs2]
  by_cases h3 : d = 3
  · subst h3; rw [hs3]; rfl
  by_cases h6 : d = 6
  · subst h6; rw [hs6]; rfl
  by_cases h7 : d = 7
  · subst h7; rw [hs7]; rfl
  by_cases h10 : d = 10
  · subst h10; rw [hs10]; rfl
  by_cases h11 : d = 11
  · subst h11; rw [hs11]
  by_cases h14 : d = 14
  · subst h14; rw [hs14]
  have g2 : swap23Class d ≠ 2 := fun h => h2 (by rw [← hinv d, h, hs2])
  have g3 : swap23Class d ≠ 3 := fun h => h7 (by rw [← hinv d, h, hs3])
  have g6 : swap23Class d ≠ 6 := fun h => h10 (by rw [← hinv d, h, hs6])
  have g7 : swap23Class d ≠ 7 := fun h => h3 (by rw [← hinv d, h, hs7])
  have g10 : swap23Class d ≠ 10 := fun h => h6 (by rw [← hinv d, h, hs10])
  have g11 : swap23Class d ≠ 11 := fun h => h11 (by rw [← hinv d, h, hs11])
  have g14 : swap23Class d ≠ 14 := fun h => h14 (by rw [← hinv d, h, hs14])
  rw [fullStarClassKernel_zero_off _ g2 g3 g6 g7 g10 g11 g14,
    fullStarClassKernel_zero_off _ h2 h3 h6 h7 h10 h11 h14]

What this page does not claim

The declaration does not prove S_RS_converges_EH_4d. The declaration does not complete the flat Hessian assembly over all hinges. The declaration 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/ReggeHinge4DStarKernel.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: