Gravity Analysis Regge Hinge4 Dstar Kernel Full Star Homothety Stationary

A stationarity checkpoint

In the study of discrete gravity, space is often built from flat blocks glued together, and curvature is measured by how much the angles around a shared edge fail to add up to a full circle. This deficit angle approach, familiar from Regge calculus, works in any dimension. In four dimensions, the shared edge is a triangle, and the question is whether a proposed rule for assigning curvature to such hinges is consistent under a simple scaling of the whole lattice.

The theorem fullStar_homothety_stationary addresses exactly that consistency. It concerns a specific hinge, the triangle spanned by the origin and two basis vectors in a four-dimensional integer lattice, and its complete periodic neighborhood, called its star. The star contains six four-simplices, the four-dimensional analog of a tetrahedron. For each of these, a local deficit kernel assigns a number to each of the fifteen possible symmetry classes of the hinge's edges. The theorem states that when these class weights are summed over all six members of the star, the total is exactly zero.

This is a stationarity condition: it says that the proposed deficit kernel is unchanged, to first order, under a uniform scaling of the lattice. Scaling every edge by a constant factor leaves the angles, and therefore the deficit angles, unchanged. The theorem confirms that the kernel respects this homothety symmetry. It is a structural check, not a dynamical one. The kernel is a definition, a choice of how to assign curvature; the theorem verifies that this choice satisfies a necessary symmetry.

The result is part of a larger program to derive gravity from a discrete, combinatorial starting point. The theorem is proved in a machine-checked library of formal theorems, meaning the derivation is verified step by step by a computer. It does not, by itself, show that this discrete model converges to Einstein's equations, nor does it determine the weights from general relativity. It is a single, rigorously checked consistency condition within a much larger construction.

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

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

What this page does not claim

This theorem does not prove convergence to general relativity. This theorem does not determine the deficit weights from the Einstein–Hilbert action. This theorem does not apply to hinges outside the specific seed triangle's periodic star.

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: