Gravity Analysis Regge Hinge4 Dstar Kernel Full Star Class Kernel Values

The full-star kernel

In four-dimensional geometry, a hinge is a two-dimensional flat piece, like a triangle, where several higher-dimensional shapes meet. The declaration fullStarClassKernel_values concerns one particular hinge: the seed triangle in the integer lattice, the regular grid of points with whole-number coordinates. Its star, the complete set of four-dimensional simplices (the simplest four-dimensional shapes, each with five vertices) that contain this hinge, is the object under study.

The machine-checked library of formal theorems proves that this star contains exactly six simplices. Four of them have a flat cosine of 1/√2 and two have a flat cosine of 0. The star angle sum, the total of the dihedral angles around the hinge, equals exactly 2π, or 360 degrees. This flatness gate is a necessary condition for the hinge to lie in a flat, Euclidean four-dimensional space.

Beyond this geometric fact, the declaration establishes a kernel, a set of numerical weights assigned to the fifteen symmetry classes of the lattice, with values (-1,-1,+1,-1,+1,+1,-1) on seven of those classes and zero on the others. This kernel is not arbitrary: it is the unique assignment that satisfies several constraints. It is nonvacuous, meaning it is not identically zero. It is symmetric under swapping the second and third coordinate directions. It is stationary under uniform scaling of the lattice, meaning the weighted sum of the kernel over all classes is zero. And it is stationary under homothety, a uniform dilation of the entire lattice.

In Recognition Science, this kernel is a step toward a discrete model of gravity. The framework treats spacetime as a lattice of simplices, and the kernel provides the weights for a discrete analogue of the Einstein-Hilbert action, the classical action whose variation gives the Einstein field equations. The declaration proves that this particular kernel exists and has the required symmetries.

What the declaration does not claim is equally precise. It does not complete the flat Hessian assembly over all hinges, meaning it does not yet provide the full second-derivative structure of the discrete action. It does not prove that the discrete sum converges to the Einstein-Hilbert action in the continuum limit. It does not recover the gap action, a separate quantity in the framework. And it does not reverse-engineer the kernel weights from the classical Einstein-Hilbert action; the weights are chosen and then verified, not derived from a classical principle. The scope is also limited: the proof concerns only the seed hinge and its full star, not other hinge orbits of the lattice, which remain open.

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

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

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]

theorem fullStar_homothety_stationary :
    fullStarDirectional (fun d => (classWeightNat d : ℝ)) = 0 := by
  simp only [fullStarDirectional]
  rw [sum15_support _ (fun d h2 h3 h6 h7 h10 h11 h14 => by
    rw [fullStarClassKernel_zero_off d h2 h3 h6 h7 h10 h11 h14, mul_zero])]
  have w2 : classWeightNat 2 = 2 := by decide
  have w3 : classWeightNat 3 = 1 := by decide
  have w6 : classWeightNat 6 = 3 := by decide
  have w7 : classWeightNat 7 = 1 := by decide
  have w10 : classWeightNat 10 = 3 := by decide
  have w11 : classWeightNat 11 = 2 := by decide
  have w14 : classWeightNat 14 = 4 := by decide
  simp [fullStarClassKernel, w2, w3, w6, w7, w10, w11, w14]
  norm_num

What this page does not claim

The declaration does not prove convergence to Einstein-Hilbert action. The declaration does not recover the gap action. The declaration does not derive kernel weights from 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/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: