Gravity Analysis Regge Hinge4 Dflat Kernel Seed Hinge Incidence Swap23

The seed hinge symmetry

In four-dimensional geometry, a simplex is the simplest shape: the analogue of a triangle in two dimensions or a tetrahedron in three. A 4-simplex has five vertices and ten edges. The Recognition Science framework builds a discrete model of spacetime from these shapes, and it needs to know how the edges of many such simplices fit together around a shared hinge, a triangle where two 4-simplices meet. The declaration seedHingeIncidence_swap23 is a proved theorem about that fitting.

The theorem states that the number of simplices containing a particular hinge is unchanged when the second and third coordinate axes are swapped. Concretely, the framework's library of formal theorems proves that the incidence count, the number of 4-simplices that contain the seed hinge, is invariant under this axis swap. The seed hinge is the triangle with vertices at the origin, the first axis, and the sum of the first two axes. The proof checks all 24 possible 4-simplices in the standard Freudenthal cell and confirms the symmetry holds for every one of the 15 edge classes. This is a combinatorial fact, not a physical one: it concerns the counting of geometric objects, not the forces or energies acting on them.

The result matters because it is a gate for a larger project. The framework's ultimate goal is to show that a discrete action, a sum over these simplices, converges to the Einstein-Hilbert action of general relativity in the smooth limit. Before that can be attempted, the combinatorial structure must be sound. This symmetry is one of the checks that the structure is consistent: if the incidence count were not invariant under the swap, the assembly would be biased toward one orientation of space, which would break the symmetry of the model. The theorem does not, however, complete the project. The true per-hinge weights, the numbers that would give each hinge its physical significance, remain an open problem. The theorem only fixes the combinatorial skeleton; the numerical content is not yet derived.

What the theorem does not claim is as important as what it proves. It does not prove that the discrete action converges to Einstein-Hilbert. It does not provide the actual weights for the hinges. It does not even establish that the model correctly describes gravity; that would require the missing kernel calculus. The declaration is a single, verified step in a long chain, a symmetry fact about counting that must hold before any physical content can be added. It is a necessary condition, not a sufficient one.

/-- THEOREM (symmetry): seed-hinge incidence is invariant under the
lattice symmetry that swaps axes `2` and `3` and fixes the hinge. -/
theorem seedHingeIncidence_swap23 (d : Fin 15) :
    seedHingeIncidenceNat (swap23Class d) = seedHingeIncidenceNat d := by
  fin_cases d <;> decide

/-- THEOREM (symmetry): seed-hinge incidence is invariant under the
lattice symmetry that swaps axes `2` and `3` and fixes the hinge. -/
theorem seedHingeIncidence_swap23 (d : Fin 15) :
    seedHingeIncidenceNat (swap23Class d) = seedHingeIncidenceNat d := by
  fin_cases d <;> decide

/-- Status record: combinatorial layer closed; true kernels OPEN. -/
structure Hinge4DFlatKernelStatus where
  freudenthal24Enumerated : Bool
  seedHingeIncidenceClosed : Bool
  trueDeficitKernelOpen : Bool
  convergesEH4d : Bool
  gapActionRecovery : Bool

What this page does not claim

This does not prove that the discrete action converges to the Einstein-Hilbert action. This does not provide numerical weights for the per-hinge deficit kernels. This does not reverse-engineer weights from Einstein-Hilbert 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/ReggeHinge4DFlatKernel.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: