Gravity Analysis Regge Hinge4 Ddihedral Kernel

The hinge kernel

In Regge calculus, spacetime is built from flat triangular pieces, and gravity is encoded in the angles where those pieces meet. The dihedral angle is the angle between two such pieces along their shared edge, called a hinge. This work studies the simplest possible four-dimensional hinge: a triangle shared by two four-simplices, the higher-dimensional analog of two tetrahedra glued along a face. The central question is how the cosine of that angle changes when the edge lengths are varied.

At the flat configuration, where all the simplices fit together without curvature, the cosine of this dihedral angle is exactly 1/√2, so the angle is 45 degrees. The established result is that the derivative of this cosine with respect to the ten edge lengths is extremely sparse: only two of the ten directions matter. Changing the length of edge 8 shifts the cosine at a rate of √2/8, changing edge 9 shifts it at −√2/4, and the other eight edges have zero effect at the flat point. This means the response to a small perturbation is concentrated on just two edges, a fact that is far from obvious from the geometry.

This derivative, packaged as the kernel (the list of rates at which the angle responds to each edge length), is the main deliverable. The local information is assembled into a deficit kernel, which tracks how the total curvature around the hinge responds. The result is again sparse: only three of the fifteen symmetry classes of edges in the lattice carry any weight, with values −1/2, −1/2, and +1/2. A uniform scaling of all edge lengths, which should leave angles unchanged, correctly gives a zero response, a check that the calculation is consistent with scale invariance.

In Recognition Science, this is a step toward deriving the Einstein–Hilbert action of general relativity from the framework's discrete ledger of recognition events. The work does not complete that derivation, and the full sum over all hinges in the lattice remains open. What it establishes is a precise, machine-checked fact about the local geometry: the exact linear response of a four-dimensional Regge hinge to its first deformation, with no approximations and no free parameters.

/-- THEOREM: flat cosine squared is `1/2` (transcendental-free form). -/
theorem cosDihedral_flat_sq :
    cosDihedral seedFlatSqEdges ^ 2 = (1 / 2 : ℝ) := by
  rw [cosDihedral_flat, div_pow, one_pow,
    Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]

lemma cosDihedralKernel_le_seven (k : Fin 10) (hk : k.val ≤ 7) :
    cosDihedralKernel k = 0 := by
  fin_cases k <;> first | rfl | exact absurd hk (by decide)

/-- THEOREM: the partial deficit kernel vanishes off classes 3, 7, 11. -/
theorem partialDeficitClassKernel_zero_off (d : Fin 15)
    (h3 : d ≠ 3) (h7 : d ≠ 7) (h11 : d ≠ 11) :
    partialDeficitClassKernel d = 0 := by
  simp only [partialDeficitClassKernel]
  rw [assembleClassKernel_eval, assembleClassKernel_eval]
  rw [show localEdgeClass 0 8 = 11 from by decide,
    show localEdgeClass 0 9 = 7 from by decide,
    show localEdgeClass 1 8 = 11 from by decide,
    show localEdgeClass 1 9 = 3 from by decide]
  rw [if_neg (show ¬((11 : Fin 15) = d) from fun h => h11 h.symm),
    if_neg (show ¬((7 : Fin 15) = d) from fun h => h7 h.symm),
    if_neg (show ¬((3 : Fin 15) = d) from fun h => h3 h.symm)]
  norm_num

/-- THEOREM (symmetry): the partial deficit class kernel is invariant
under the hinge-fixing axis swap `2 ↔ 3` of the incidence layer. -/
theorem partialDeficitClassKernel_swap23 (d : Fin 15) :
    partialDeficitClassKernel (swap23Class d) =
      partialDeficitClassKernel d := by
  have hinv : ∀ x : Fin 15, swap23Class (swap23Class x) = x := by decide
  have hs3 : swap23Class 3 = 7 := by decide
  have hs7 : swap23Class 7 = 3 := by decide
  have hs11 : swap23Class 11 = 11 := by decide
  by_cases h3 : d = 3
  · subst h3
    rw [hs3, partialDeficitClassKernel_seven, partialDeficitClassKernel_three]
  by_cases h7 : d = 7
  · subst h7
    rw [hs7, partialDeficitClassKernel_three, partialDeficitClassKernel_seven]
  by_cases h11 : d = 11
  · subst h11
    rw [hs11]
  have g3 : swap23Class d ≠ 3 := fun h => h7 (by rw [← hinv d, h, hs3])
  have g7 : swap23Class d ≠ 7 := fun h => h3 (by rw [← hinv d, h, hs7])
  have g11 : swap23Class d ≠ 11 := fun h => h11 (by rw [← hinv d, h, hs11])
  rw [partialDeficitClassKernel_zero_off _ g3 g7 g11,
    partialDeficitClassKernel_zero_off _ h3 h7 h11]

What this page does not claim

This work does not prove that the full Regge action converges to the Einstein–Hilbert action in four dimensions. This work does not complete the flat Hessian of the 4D Regge action. This work does not derive the weights of the action from first principles.

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