Gravity Analysis Regge Hinge4 Dstar Kernel22

A flat hinge in four dimensions

In four-dimensional geometry, a hinge is a two-dimensional plane where several volumes meet, like the spine of a book where pages of different thicknesses come together. Regge calculus, a standard method in numerical relativity, builds curved spacetime by gluing flat four-dimensional blocks together and measuring how much angle is missing around each hinge. That missing angle, the deficit angle, is the discrete stand-in for curvature.

The module ReggeHinge4DStarKernel22 in the framework's machine-checked library of formal theorems examines one specific hinge, called type (2,2), in a periodic lattice of four-dimensional cubes. It proves, by decidable computation, that exactly four cube-and-simplex pairs contain this hinge, and that in its flat configuration all four incident simplices have zero cosine for the dihedral angle. The star angle sum is exactly 2π, the flat-space value. The module then assembles a full-star deficit class kernel, a table of 15 numbers describing how the deficit angle responds to small changes in the edge lengths, and proves it is symmetric under two coordinate swaps and stationary under uniform scaling.

In Recognition Science, this is a step in a larger campaign to show that Einstein–Hilbert gravity emerges from the framework's discrete ledger of recognition events. The module does not complete that derivation. It does not prove that the framework's action converges to Einstein–Hilbert in four dimensions, and it does not recover the weights of general relativity from the deficit kernel. What it establishes is a precise, machine-checked fact: this particular hinge, in its flat state, has a well-defined, symmetric, non-vacuous response kernel. The result is a building block, not the building.

The proof is axiom-clean, using only the standard axioms of the ambient type theory. The significance for a working physicist is that the discrete geometry of a four-dimensional lattice has a controlled, computable flat limit at this hinge. For the framework, it is a verified increment in a long chain: one hinge's kernel, checked, before the next hinge orbit is attempted.

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

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

theorem fullStarClassKernel_swap01 (d : Fin 15) :
    fullStarClassKernel (swap01Class d) = fullStarClassKernel d := by
  fin_cases d <;> rfl

theorem fullStarClassKernel_swap23 (d : Fin 15) :
    fullStarClassKernel (swap23Class 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 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]
  norm_num

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

What this page does not claim

The module does not prove that the framework's action converges to Einstein–Hilbert in four dimensions. The module does not recover the weights of general relativity from the deficit kernel. The module does not complete the flat Hessian assembly over all hinges.

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