Gravity Analysis Regge Hinge4 Ddihedral Kernel Hinge4 Ddihedral Kernel Status Fl

A kernel for one hinge

In Regge calculus, spacetime is chopped into flat simplexes, and gravity is encoded in the angles where these simplexes meet. The declaration hinge4DDihedralKernelStatus_flags concerns one such meeting place, a hinge, in four dimensions. It establishes, as a proved theorem, the exact rate at which the cosine of the dihedral angle at that hinge changes when the ten surrounding squared edge lengths are varied slightly. This rate, the kernel, is not a vague approximation but a precise list of ten numbers, one for each edge.

The calculation is done at a specific reference point, the flat Freudenthal point, where the geometry is regular. At that point, the cosine of the dihedral angle is proved to equal 1 divided by the square root of 2, a familiar value for a right angle in four dimensions. The kernel itself is sparse: of the ten possible edge directions, only two have a non-zero effect on the cosine. Varying edge number eight changes the cosine at a rate of the square root of 2 divided by 8, while varying edge number nine changes it at the rate of the negative square root of 2 divided by 4. The other eight edges have no effect at all, a result proved directly from the definitions. This sparsity is the core finding: a single hinge's angle responds to only two of its ten defining lengths, at least at the flat point.

From this cosine kernel, the declaration derives the corresponding kernel for the angle itself and for the two-simplex partial deficit, a quantity related to curvature. These derived kernels inherit the same sparsity, being supported on only three of the fifteen edge classes. The declaration also proves that the kernel is not zero, that it is symmetric under swapping two specific axes, and that it correctly gives zero for a uniform scaling of all lengths, as scale invariance demands. All of this is verified in a machine-checked library of formal theorems, meaning the proofs are checked step-by-step by a computer and rely only on the standard axioms of logic.

In Recognition Science, this is a building block, not a final result. The declaration explicitly does not claim to have completed the full Hessian of the four-dimensional Regge action, nor does it prove that the Regge action converges to the Einstein-Hilbert action. It does not attempt to recover the action's weights from general relativity. The scope is deliberately narrow: the kernel is computed only for the seed hinge within its two seed-cell simplices, not for the full lattice of all possible hinges. The sum over all hinges remains an open target. What the declaration provides is a rigorously checked, local piece of the larger program, a precise answer for one hinge that can serve as a foundation for subsequent steps.

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

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

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 (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

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

/-- 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 declaration does not complete the flat Hessian of the 4D Regge action. This declaration does not prove that the Regge action converges to the Einstein-Hilbert action. This declaration does not derive the weights of the Regge action by matching 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: