Gravity Analysis Regge Hinge4 Dstar Kernel13 Hinge4 Dstar Kernel13 Status Flags

A flat hinge in four dimensions

In four-dimensional geometry, a simplex is the simplest shape: a 4-simplex has five corners, ten edges, and ten triangular faces. When several simplices share a common edge, that edge is called a hinge, and the way the simplices fold around it determines the local curvature of the whole assembly. The declaration in question proves that for one particular type of hinge, in a periodic lattice of unit cubes, the surrounding simplices lie perfectly flat: the angles around the hinge sum to exactly 2π, the full circle.

The proof works by exhaustive enumeration. In the origin unit cube, exactly six simplices contain the hinge, and among all neighboring cube translates, only the origin cube does. Each of these six simplices has a flat cosine of 1/2, meaning each contributes an angle of π/3. Six times π/3 is 2π, so the hinge is flat. The declaration also computes all ten coordinate derivatives of the cosine function at this flat configuration, and assembles a full kernel over the 15 possible edge classes, with values like −√3 and +√3. Several consistency gates pass: the configuration is nonempty, symmetric under swapping two axes, and stationary under uniform scaling.

This is a kernel-checked theorem in the framework's machine-checked library of formal theorems. It is a technical but necessary step: before one can ask whether a discrete lattice approximates Einstein's equations of gravity, one must know which configurations are flat. This declaration establishes that this particular hinge, of type (1,3), is flat in the periodic lattice. The complementary type (3,1) is related by a symmetry, but transporting this result to that case remains an open problem.

What this declaration does not do is equally important. It does not complete the full assembly of the Hessian, the matrix of second derivatives, over all hinges. It does not prove that the discrete action converges to the Einstein–Hilbert action of general relativity. It does not recover the coupling constants of gravity from first principles. It is one verified brick in a wall, not the wall itself.

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

theorem star_cardinality :
    (Finset.univ.filter (fun s : Fin 24 => containsHinge s = true)).card =
      6 := by
  decide

theorem only_origin_contains_hinge :
    (Finset.univ.filter (fun c : CubeOffset =>
      cubeContainsHinge c = true)) = {originOffset} := by
  decide

theorem hasDerivAt_t13_coord (k : Fin 10) :
    HasDerivAt (fun t : ℝ => cosDihedral (t13CoordPath k t))
      (t13CosKernel k) (t13FlatSqEdges k) := by
  fin_cases k
  · exact hasDerivAt_t13_slot0
  · exact hasDerivAt_t13_slot1
  · exact hasDerivAt_t13_slot2
  · exact hasDerivAt_t13_slot3
  · exact hasDerivAt_t13_slot4
  · exact hasDerivAt_t13_slot5
  · exact hasDerivAt_t13_slot6
  · exact hasDerivAt_t13_slot7
  · exact hasDerivAt_t13_slot8
  · exact hasDerivAt_t13_slot9

theorem fullStar_homothety_stationary :
    fullStarDirectional (fun d => (classWeightNat d : ℝ)) = 0 := by
  simp only [fullStarDirectional]
  rw [sum15_support _ (fun d h1 h3 h5 h7 h9 h11 h13 => by
    rw [fullStarClassKernel_zero_off d h1 h3 h5 h7 h9 h11 h13, mul_zero])]
  have w1 : classWeightNat 1 = 1 := by decide
  have w3 : classWeightNat 3 = 1 := by decide
  have w5 : classWeightNat 5 = 2 := by decide
  have w7 : classWeightNat 7 = 1 := by decide
  have w9 : classWeightNat 9 = 2 := by decide
  have w11 : classWeightNat 11 = 2 := by decide
  have w13 : classWeightNat 13 = 3 := by decide
  simp [fullStarClassKernel, w1, w3, w5, w7, w9, w11, w13]
  ring

What this page does not claim

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