Gravity Analysis Regge Hinge4 Dstar Kernel22 Star Flat Cosines Match Orbit

The flat star check

In four-dimensional geometry, a hinge is a line segment where two triangles meet, like the spine of an open book. In a curved space, the angles around a hinge do not add up to a full circle; the shortfall is called the deficit angle, and it measures the local curvature. The declaration starFlatCosines_match_orbit is a machine-checked proof that, for one particular four-dimensional configuration, all four triangles meeting at a hinge are perfectly flat, meaning their dihedral angles are all right angles.

The configuration is a specific type of four-dimensional simplex, a triangle-like shape with five corners, arranged in a periodic lattice. The proof establishes that exactly four such simplices contain the hinge, and that each one contributes a cosine of zero, which corresponds to an angle of 90 degrees. The sum of the four angles is therefore exactly 2π, or a full circle, showing that the space is locally flat at that hinge. This is a precise, computational result, verified by the machine-checked library of formal theorems, not a numerical approximation.

This result is part of a larger effort to build a theory of quantum gravity from discrete geometry. The declaration is a technical but necessary step: it verifies that a particular building block behaves as expected. It does not, however, assemble the full picture. The proof does not show that the entire space is flat, only that this one hinge is. It does not prove that this discrete geometry converges to Einstein's theory of general relativity, and it does not derive the weights of the geometry from first principles.

What the declaration does provide is a solid, verified foundation stone. It confirms that a specific piece of the geometric machinery is consistent and flat, allowing the next stages of the construction to proceed on a checked basis. This is the nature of the work: one exact, local fact at a time, building toward a global theory.

theorem starFlatCosines_match_orbit (m : Fin 4) :
    starFlatCosines m = cosDihedral t22FlatSqEdges :=
  cosDihedral_t22_flat.symm

theorem star_cardinality :
    (Finset.univ.filter (fun p : CubeCorner × Fin 24 =>
      containsHinge p.1 p.2 = true)).card = 4 := by
  decide

theorem starFlatCosines_match_orbit (m : Fin 4) :
    starFlatCosines m = cosDihedral t22FlatSqEdges :=
  cosDihedral_t22_flat.symm

theorem star_flat_angle_sum_two_pi : starFlatAngleSum = 2 * Real.pi := by
  simp only [starFlatAngleSum, flatAngleT22_eq]
  ring

What this page does not claim

This proof does not establish that the entire four-dimensional space is flat, only that a single hinge is locally flat. This proof does not demonstrate convergence to Einstein's general relativity. This proof does not derive the geometric weights from first principles.

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