Gravity Analysis Regge Hinge4 Dstar Kernel Full Star Class Kernel Nonvacuous

The nonempty kernel

In the framework's approach to gravity, space is not a smooth fabric but a discrete lattice of points, and curvature is measured by how much the angles around a hinge fail to sum to a flat 360 degrees. The declaration fullStarClassKernel_nonvacuous is a machine-checked proof that this curvature response, called a kernel, is not empty: at least one of the fifteen possible angle classes produces a nonzero value. This matters because a kernel that is all zeros would mean the geometry has no reaction to deformation, making any further analysis pointless.

The proof examines a specific geometric object: a seed triangle hinge, which is a line segment where two triangular faces meet, surrounded by its full periodic star in the four-dimensional integer lattice. This star consists of exactly six unit cubes and six four-dimensional simplices that contain the hinge. The kernel assigns a real number to each of the fifteen angle classes, and the theorem proves the value at class 11 is not zero. This is not a calculation of a physical quantity; it is a logical gate that confirms the mathematical object is well-formed and has the expected structure.

The declaration is part of a larger campaign to build a discrete theory of gravity from the framework's axioms. It follows an earlier proof about the dihedral angle of a single hinge and uses the same incidence geometry. The kernel is assembled from six local contributions, one for each simplex in the star, and the theorem verifies that the assembled object is not identically zero. The proof is checked by a machine, meaning no step is left to human intuition, and it relies only on the standard logical axioms of the underlying type theory.

What the declaration does not claim is as important as what it proves. It does not show that the full curvature matrix over all hinges is flat or complete. It does not prove that the framework's action converges to the Einstein-Hilbert action of general relativity. It does not recover the weights that would make the discrete theory match classical gravity. It only establishes that this particular kernel, for this particular hinge in this particular lattice, has at least one nonzero entry. This is a necessary condition for the larger project, but it is far from sufficient.

The practical consequence is that the framework has a verified foothold in four-dimensional discrete geometry. The next steps remain open: assembling the full flat Hessian over all hinges, proving convergence to general relativity, and deriving the physical coupling constants. Each of these is a target, not an achievement. The nonvacuous kernel is a single checked brick in a wall that is still mostly unbuilt.

theorem fullStarClassKernel_nonvacuous : fullStarClassKernel 11 ≠ 0 := by
  norm_num [fullStarClassKernel]

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

def fullStarClassKernelAssembled : Fin 15 → ℝ :=
  fun d => ∑ m : Fin 6, assembleStarMember m d

What this page does not claim

The declaration does not prove the full flat Hessian assembly over all hinges is complete. The declaration does not establish convergence to the Einstein-Hilbert action of general relativity. The declaration does not reverse-engineer the kernel weights from classical gravity.

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