Gravity Analysis Regge Hinge4 Dstar Kernel12

A flat hinge in four dimensions

In the geometry of spacetime, a hinge is a line segment where two triangles meet, like the spine of an open book. In four dimensions, a hinge is where two tetrahedra meet, a triangle. The module ReggeHinge4DStarKernel12 examines one particular hinge in a four-dimensional lattice, the triangle with vertices at {0, e₀, e₀+e₁+e₂}, and proves that the four tetrahedra surrounding it lie perfectly flat, like a book opened all the way to 360 degrees.

The proof works by counting. Around this hinge, exactly four tetrahedra fit, two from one unit cube and two from a neighboring cube. The module proves this count is exactly four, no more and no less. For each of these four tetrahedra, it computes the dihedral angle at the hinge using a Gram matrix, a standard tool from linear algebra that encodes the lengths and angles between edges. In all four cases, the cosine of the angle is exactly 0, meaning each angle is exactly 90 degrees. Four times 90 degrees is 360 degrees, so the hinge is flat, with no curvature.

The module then builds a kernel, a function that assigns a value to each of 15 possible edge-length classes in the lattice. This kernel takes values of either +√2/2 or −√2/2, and it satisfies a symmetry: swapping the roles of the two non-hinge edges leaves the kernel unchanged. It also responds predictably to scaling: if you multiply all edge lengths by a constant, the kernel's value stays the same, a property called homothety stationarity.

In Recognition Science, this is a step toward showing that gravity, the curvature of spacetime, can be derived from a discrete ledger of recognition events. The flatness of this hinge is a local check, a single tile in a much larger mosaic. The module does not prove that the full assembly of all hinges gives Einstein's equations, nor does it derive the fine-structure constant. It is a precise, machine-checked fact about one piece of the lattice, a fact that any complete theory of discrete gravity must respect.

The importance is not the hinge itself, but the method. The proof is checked by a machine, with no gaps and no hidden assumptions, using only the standard axioms of logic. This means the flatness result is not a guess or an approximation; it is a theorem. It demonstrates that the framework's geometric calculus can produce exact, verifiable statements about the structure of spacetime, one hinge at a time.

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

def starFlatCosines : Fin 4 → ℝ
  | _ => 0

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

theorem fullStarClassKernel_swap12 (d : Fin 15) :
    fullStarClassKernel (swap12Class d) = fullStarClassKernel d := by
  fin_cases d <;> rfl

theorem fullStar_homothety_stationary :
    fullStarDirectional (fun d => (classWeightNat d : ℝ)) = 0 := by
  simp only [fullStarDirectional]
  rw [sum15_all]
  have hs : Real.sqrt 2 ≠ 0 := Real.sqrt_ne_zero'.mpr (by norm_num)
  have w0 : classWeightNat 0 = 1 := by decide
  have w1 : classWeightNat 1 = 1 := by decide
  have w2 : classWeightNat 2 = 2 := by decide
  have w3 : classWeightNat 3 = 1 := by decide
  have w4 : classWeightNat 4 = 2 := by decide
  have w5 : classWeightNat 5 = 2 := by decide
  have w6 : classWeightNat 6 = 3 := by decide
  have w7 : classWeightNat 7 = 1 := by decide
  have w8 : classWeightNat 8 = 2 := by decide
  have w9 : classWeightNat 9 = 2 := by decide
  have w10 : classWeightNat 10 = 3 := by decide
  have w11 : classWeightNat 11 = 2 := by decide
  have w12 : classWeightNat 12 = 3 := by decide
  have w13 : classWeightNat 13 = 3 := by decide
  have w14 : classWeightNat 14 = 4 := by decide
  simp [fullStarClassKernel, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9,
    w10, w11, w12, w13, w14]
  field_simp
  ring

What this page does not claim

This module does not prove that the full assembly of all hinges gives Einstein's equations. This module does not derive the fine-structure constant or any other coupling constant. This module does not claim that the hinge is flat in all possible four-dimensional lattices, only in this specific periodic lattice.

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