Gravity Analysis Regge Hinge4 Ddihedral Kernel Single Simplex Deficit Kernel Eig

The single-simplex deficit kernel

In Regge calculus, a discrete approach to general relativity, space is built from flat pieces glued along hinges. The deficit angle measures how much the pieces fail to lie flat around a hinge. This declaration concerns one seed triangle hinge inside a four-simplex, the four-dimensional analogue of a triangle. The theorem singleSimplexDeficitKernel_eight states that, at the flat configuration, the rate of change of the deficit angle with respect to the squared length of edge slot 8 equals exactly one quarter. Edge slot 9 changes at minus one half, and all other eight slots change at zero.

The numbers come from a chain of definitions. The cosine of the dihedral angle is expressed as an explicit function of the ten squared edge lengths. At the flat point, this cosine equals 1/√2, meaning the angle is 45 degrees. The derivative of this cosine with respect to each edge is then computed. The theorem hasDerivAt_cosDihedral_coord proves these derivatives are correct. The deficit kernel, a list of ten numbers giving the gradient of the deficit angle, is then obtained by multiplying the cosine derivatives by the chain rule factor −√2, which is −1/sin(45°).

The result is local. It applies only to the seed hinge inside its two seed-cell Freudenthal 4-simplices, not to the full lattice of hinges in a large triangulation. The full orbit sum over all hinges remains open. The theorem does not complete the flat Hessian of the 4D Regge action, does not prove that the Regge action converges to Einstein–Hilbert, and does not reverse-engineer weights from Einstein–Hilbert. The proof is machine-checked in the framework's library of formal theorems, with no unproved assumptions beyond the standard axioms of the ambient type theory.

What this establishes is a precise, verified ingredient for a larger campaign. It gives the exact linear response of one geometric quantity to changes in edge lengths at one special configuration. That is a concrete step toward understanding how the discrete action behaves, not a claim about the full theory. The value one quarter is not fitted or assumed; it is derived from the definitions and checked by the kernel.

theorem singleSimplexDeficitKernel_eight :
    singleSimplexDeficitKernel 8 = (1 / 4 : ℝ) := by
  simp only [singleSimplexDeficitKernel]
  rw [angleKernel_eight]
  norm_num

theorem singleSimplexDeficitKernel_nine :
    singleSimplexDeficitKernel 9 = (-1 / 2 : ℝ) := by
  simp only [singleSimplexDeficitKernel]
  rw [angleKernel_nine]
  norm_num

theorem singleSimplexDeficitKernel_le_seven (k : Fin 10) (hk : k.val ≤ 7) :
    singleSimplexDeficitKernel k = 0 := by
  simp [singleSimplexDeficitKernel, angleKernel,
    cosDihedralKernel_le_seven k hk]

/-- 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)]

/-- 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 result applies only to one seed hinge, not to the full lattice of hinges. The theorem does not prove convergence of the Regge action to Einstein–Hilbert. The kernel values are derived, not fitted to match general relativity.

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: