Gravity Analysis Regge Hinge4 Ddihedral Kernel Single Simplex Deficit Kernel Le

A narrow zero result

In four-dimensional geometry, a simplex is the simplest shape: a tetrahedron-like object with five corners. A Regge calculus approach approximates curved spacetime by gluing many such flat simplices together, measuring curvature by how much the angles around shared edges fail to sum to a flat value. The declaration singleSimplexDeficitKernel_le_seven concerns one such angle, the dihedral angle between two faces of a single simplex, and how it responds when the lengths of the simplex's edges are varied.

The result is a precise statement about a derivative, a measure of sensitivity. At a specially chosen flat configuration, the derivative of the cosine of the dihedral angle with respect to seven of the ten squared edge lengths is exactly zero. In plainer terms, wiggling those seven edge lengths, one at a time, leaves the angle unchanged to first order. Only the eighth and ninth edge lengths matter at this flat point, with the derivative taking values of √2/8 and -√2/4 respectively. This is a local statement, valid only at that one flat point, not a global property of all simplices.

The ledger, a discrete record of geometric events, here tracks the ten edge lengths and their influence on the angle. The result is a kernel, a list of ten numbers showing how each edge length affects the angle. The theorem proves that seven of these ten entries are zero, a fact that simplifies later calculations by showing which directions truly matter. It also confirms a symmetry: swapping two specific edge labels leaves the kernel unchanged, and uniformly scaling all lengths produces a zero response, as expected for a scale-invariant angle.

This is a small, tightly scoped step. It does not describe the full curvature of a four-dimensional spacetime, nor does it prove that this discrete approach converges to Einstein's equations. The result concerns only a single simplex at a single flat configuration, not the sum over the entire lattice of simplices that a complete theory would require. The full orbit sum over all hinges remains an open target. The declaration is a building block, verified by a machine-checked library of formal theorems, not a standalone theory of gravity.

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)

lemma cosDihedralKernel_eight : cosDihedralKernel 8 = Real.sqrt 2 / 8 := rfl

lemma cosDihedralKernel_nine : cosDihedralKernel 9 = -(Real.sqrt 2) / 4 := rfl

/-- THEOREM (deliverable A): every local squared-length direction has an
explicit flat cosine derivative given by `cosDihedralKernel`. -/
theorem hasDerivAt_cosDihedral_coord (k : Fin 10) :
    HasDerivAt (fun t : ℝ => cosDihedral (coordPath k t))
      (cosDihedralKernel k) (seedFlatSqEdges k) := by
  fin_cases k
  · exact hasDerivAt_cosDihedral_slot0
  · exact hasDerivAt_cosDihedral_slot1
  · exact hasDerivAt_cosDihedral_slot2
  · exact hasDerivAt_cosDihedral_slot3
  · exact hasDerivAt_cosDihedral_slot4
  · exact hasDerivAt_cosDihedral_slot5
  · exact hasDerivAt_cosDihedral_slot6
  · exact hasDerivAt_cosDihedral_slot7
  · exact hasDerivAt_cosDihedral_slot8
  · exact hasDerivAt_cosDihedral_slot9

What this page does not claim

The declaration does not prove that the full 4D Regge action converges to Einstein's equations. The declaration does not describe the behavior of the angle away from the flat configuration. The declaration does not cover the sum over all simplices in a lattice, only a single simplex.

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: