Gravity Analysis Regge Hinge4 Ddihedral Kernel Cos Dihedral Homothety Stationary

The flat dihedral kernel

In four-dimensional geometry, a dihedral angle is the angle between two flat faces that meet along a common edge, much as two walls of a room meet along a corner. The declaration cosDihedral_homothety_stationary concerns a specific such angle inside a four-dimensional simplex, the simplest possible four-dimensional shape, built from five points. The framework's machine-checked library of formal theorems proves that when all ten edge lengths of this simplex are scaled uniformly, the cosine of this dihedral angle does not change. A uniform scaling stretches the whole shape like a balloon, and the angle between its faces stays fixed, which is exactly what scale invariance demands.

The calculation is not abstract. The library works with a concrete seed simplex, the one whose vertices are at the origin and the first two standard basis vectors, and it tracks the ten squared edge lengths as a list of ten numbers. At the flat point, where the simplex is as close to flat as a four-dimensional shape can be, the cosine of the dihedral angle equals 1/√2, so the angle itself is 45 degrees. The derivative of this cosine with respect to each of the ten edge lengths is computed exactly: eight of the ten derivatives are zero, one is √2/8, and the last is -√2/4. These ten numbers form the kernel, the local response of the angle to changes in the edges.

The homothety statement is a check on this kernel. A homothety is a uniform scaling of all edge lengths by the same factor, and the derivative along that direction must be zero because the angle does not change under scaling. The library computes this directional derivative directly from the ten kernel entries and proves it equals zero exactly, not by assumption but by calculation. It also proves a decoy direction, one that scales only a single edge, gives a nonzero derivative, so the zero result is not vacuous. This confirms the kernel is internally consistent with the geometric fact that angles are scale-invariant.

In Recognition Science, this result is a step toward a larger goal: showing that a discrete, combinatorial model of spacetime, built from simplices like this one, reproduces the curvature of general relativity. The framework models gravity not as a continuous field but as a collection of flat pieces hinged along edges, and the dihedral angle is the hinge. This declaration proves the local response of that hinge to edge-length changes at the flat point. It does not prove the full theory. The sum over all hinges in the entire lattice is an open target, and the flat Hessian of the four-dimensional Regge action, the second derivative that would give the full curvature, is not completed by this result.

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

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

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 model converges to general relativity. This does not reverse-engineer weights from Einstein-Hilbert.

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: