Gravity Analysis Regge Hinge4 Ddihedral Kernel Partial Deficit Class Kernel Valu

The partial deficit kernel

In four-dimensional geometry, a simplex is the simplest shape with five corners, and its dihedral angle is the angle between two of its four-dimensional faces. The deficit angle at a hinge is the amount by which the sum of these dihedral angles falls short of a full circle; it is the quantity that measures curvature in Regge calculus, a discrete approach to gravity. A machine-checked library of formal theorems has now established the gradient of this deficit angle at a flat configuration, for one seed hinge inside two specific simplexes.

The calculation begins with the cosine of the dihedral angle, 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 the cosine with respect to each of the ten edge lengths is then computed: it is zero for eight of them, √2/8 for slot 8, and -√2/4 for slot 9. From these, the derivative of the deficit angle itself follows by the chain rule, giving values of -1/4 and 1/2 for those two slots.

These local derivatives are then assembled across the fifteen edge classes of the two simplexes. The result, called the partial deficit class kernel, is supported on only three classes, with values (-1/2, -1/2, +1/2). This means that stretching edges in those three classes changes the total deficit angle in a precise, simple way, while stretching edges in the other twelve classes leaves it unchanged. The kernel is also shown to be invariant under swapping two of the axes, and it correctly gives zero when all edge lengths are scaled uniformly, as scale invariance requires.

In Recognition Science, this is a step toward deriving the discrete action of gravity from first principles. The framework models spacetime as a discrete ledger of recognition events, and this calculation provides a kernel-checked piece of the curvature that such a ledger would generate. The result is a theorem, proved with no axioms beyond the standard logical ones, but its scope is deliberately narrow: it covers only one seed hinge inside two specific simplexes, not the full lattice of all hinges.

What this establishes is a concrete, verified fact about how a geometric quantity responds to edge-length variation. It does not complete the full Hessian of the 4D Regge action, it does not prove that the discrete action converges to the Einstein-Hilbert action, and it does not reverse-engineer weights from general relativity. The value is a building block, not the building.

/-- 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_eight : cosDihedralKernel 8 = Real.sqrt 2 / 8 := rfl

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

/-- 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 (nonvacuity): the slot-9 cosine kernel is nonzero. -/
theorem cosDihedralKernel_nonvacuous : cosDihedralKernel 9 ≠ 0 := by
  rw [cosDihedralKernel_nine]
  have h2 : (0 : ℝ) < Real.sqrt 2 := Real.sqrt_pos.mpr (by norm_num)
  intro h
  linarith

What this page does not claim

This does not complete the flat Hessian of the 4D Regge action. This does not prove that the discrete action converges to the Einstein-Hilbert action. This does not reverse-engineer weights from 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: