Gravity Analysis Regge Hinge4 Dstar Kernel12 Star Flat Cosines Match Orbits

The flat star check

In four-dimensional geometry, a simplex is the simplest shape built from five points, the analog of a triangle in two dimensions or a tetrahedron in three. A hinge is the lower-dimensional piece where two such simplices meet, like an edge where two triangles join. The declaration starFlatCosines concerns a specific hinge in the four-dimensional integer lattice, the grid of points with whole-number coordinates, and the four simplices that surround it.

The proof establishes a clean geometric fact. For this particular hinge, the four surrounding simplices each have a flat cosine of zero, meaning the angle at the hinge is a right angle, π/2 radians. The star angle sum, the total of these four angles, is exactly 2π, a full turn. The result is part of a larger machine-checked library of formal theorems, where every statement is verified by a computer from first principles. The proof also confirms that exactly four such simplices contain the hinge, and that the collection is symmetric under a swap of two coordinate directions.

In Recognition Science, this geometric check is a kernel for a proposed discrete model of gravity. The framework models spacetime as a lattice of discrete events, and this declaration tests whether a particular local configuration is flat, meaning it has zero curvature. The result is a necessary building block: a flat local patch that can be used to assemble larger structures. The framework's library shows that this patch is consistent, but it does not yet show that the full theory reproduces Einstein's equations of general relativity.

The declaration does not claim that the entire discrete gravity theory is complete or correct. It does not prove that the sum over all such hinges converges to the Einstein-Hilbert action, the standard mathematical description of gravity. It does not determine the weights that would make the model match known physics. It only establishes the local flatness of one specific configuration, a single verified step in a much longer chain of reasoning.

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

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

def starFlatCosines : Fin 4 → ℝ
  | _ => 0

What this page does not claim

The declaration does not prove that the discrete gravity theory converges to Einstein-Hilbert gravity. The declaration does not derive the weights that would match observed gravitational physics. The declaration does not cover other hinge types in the four-dimensional lattice.

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