Gravity Analysis Regge Hinge4 Dstar Kernel22 Full Star Class Kernel Swap01

A symmetry in the star kernel

In four-dimensional geometry, a hinge is a flat two-dimensional surface where several four-dimensional volumes meet, like the edge where pages of a book come together. The declaration fullStarClassKernel_swap01 concerns a specific hinge and the collection of all volumes around it, called its star. The proof establishes that this star's kernel, a numerical measure of how the geometry bends at the hinge, is unchanged when the first two coordinates of the space are swapped. This is a symmetry: the geometry looks the same from two different perspectives.

The setting is a four-dimensional lattice, a regular grid of points extending in all directions. The hinge in question is a triangle with vertices at the origin and two other lattice points. Around this hinge, exactly four four-dimensional volumes (called simplices) meet. The proof verifies that this star is complete, meaning no other volumes touch the hinge, and that the hinge is flat: the angles around it sum to exactly 2π, the same as a full circle in a plane. The kernel is a list of numbers, one for each of the 15 possible symmetry classes of nearby lattice points, and the theorem states that swapping the first two coordinates leaves this list unchanged.

This symmetry is not an accident of the specific hinge chosen. The proof checks the property for every one of the 15 classes, using a computer-verified calculation. It also holds under a different swap, of the third and fourth coordinates. These symmetries reflect the underlying structure of the four-dimensional lattice and are expected to be important for understanding how gravity might emerge from a discrete lattice, a topic the framework investigates. The result is a small but rigorous step in a larger program.

The declaration does not make broader claims. It does not prove that this kernel, or any combination of kernels, equals the Einstein-Hilbert action of general relativity. It does not establish that a sum over all hinges converges to that action. It does not recover the weights of the lattice from the action. It only establishes a symmetry property for this one hinge's star. The machine-checked library of formal theorems confirms the proof is valid, but the physical interpretation remains a subject of ongoing work.

theorem fullStarClassKernel_swap01 (d : Fin 15) :
    fullStarClassKernel (swap01Class d) = fullStarClassKernel d := by
  fin_cases d <;> rfl

theorem star_cardinality :
    (Finset.univ.filter (fun p : CubeCorner × Fin 24 =>
      containsHinge p.1 p.2 = true)).card = 4 := by
  decide

theorem star_flat_angle_sum_two_pi : starFlatAngleSum = 2 * Real.pi := by
  simp only [starFlatAngleSum, flatAngleT22_eq]
  ring

theorem fullStarClassKernel_swap01 (d : Fin 15) :
    fullStarClassKernel (swap01Class d) = fullStarClassKernel d := by
  fin_cases d <;> rfl

What this page does not claim

This declaration does not prove that the star kernel equals the Einstein-Hilbert action. This declaration does not establish convergence of a sum over all hinges to a gravitational action. This declaration does not recover lattice weights from the Einstein-Hilbert action.

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