Gravity Analysis Regge Hinge4 Dstar Kernel Full Star Class Kernel Zero Off

The full-star class kernel

In four-dimensional geometry, a hinge is a two-dimensional triangle where several four-dimensional simplexes meet, like the crease where multiple facets of a crystal meet along an edge. The declaration fullStarClassKernel_zero_off concerns the complete set of simplexes around such a hinge in a regular lattice: a discrete, repeating arrangement of points in four-dimensional space. The framework's machine-checked library of formal theorems proves that exactly six simplexes contain this seed hinge, and that the six flat dihedral angles around it sum to exactly 2π, the full angle around a point in a flat plane.

From this flatness gate, the library derives a specific assignment of weights, called the full-star class kernel, to the fifteen symmetry classes of edges in the lattice. The kernel takes the values (-1, -1, +1, -1, +1, +1, -1) on seven of these classes and zero on the remaining eight. This is not a guess: the declaration proves this kernel is nonvacuous, meaning it is not identically zero, and that it is symmetric under swapping two of the coordinate directions. The kernel also passes a homothety stationarity test, meaning that uniformly scaling the lattice leaves its directional sum unchanged.

In Recognition Science, this kernel is a step toward building a discrete model of gravity, where curvature is measured by angle deficits around hinges, much as a cone's tip has a total angle less than 2π. The framework models this by assigning deficit weights to edge classes, and the full-star kernel is the first complete, kernel-checked assignment for this hinge orbit. The declaration establishes that this particular assignment is internally consistent and satisfies the flatness condition for the seed hinge.

What the declaration does not claim is just as important. It does not complete the assembly of the flat Hessian over all hinges in the lattice, which would be needed for a full discrete action. It does not prove that the Recognition Science action converges to the Einstein-Hilbert action of general relativity. It does not derive the weights by reverse-engineering them from known physics, and it does not settle the behavior of any other hinge orbit in the lattice. Those remain open targets for the framework.

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

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

theorem fullStarClassKernel_nonvacuous : fullStarClassKernel 11 ≠ 0 := by
  norm_num [fullStarClassKernel]

theorem fullStarClassKernel_nonvacuous : fullStarClassKernel 11 ≠ 0 := by
  norm_num [fullStarClassKernel]

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 complete the flat Hessian assembly over all hinges. The declaration does not prove convergence to the Einstein-Hilbert action. The declaration does not reverse-engineer weights from known physics.

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: