Gravity Analysis Regge Hinge4 Dflat Kernel Seed Hinge Incidence Nat Values

Counting a seed hinge

In four-dimensional geometry, a simplex is the simplest shape: the four-dimensional analogue of a triangle, with five vertices and ten edges. The declaration seedHingeIncidenceNat counts, for each of fifteen edge classes, how many of the two selected simplices contain that class as a local edge. The two simplices are the ones that contain a particular triangle, called the seed hinge, with vertices at positions 0, e₀, and e₀+e₁. The count is a plain natural number: 0, 1, or 2.

The framework's machine-checked library of formal theorems proves several facts about this count. The total sum of counts across all fifteen classes is 20. The count is nonzero for the three hinge-boundary classes, meaning those edge classes do appear in the support. Three other classes, labeled 4, 8, and 12, are decoys: their count is exactly zero, so they never appear in either of the two simplices. The count is also symmetric under swapping the third and fourth axes, a symmetry that fixes the seed hinge itself. These results are combinatorial, meaning they follow from the explicit enumeration of the 24 monotone 4-simplices, not from any physical assumption.

In Recognition Science, this counting table is a step toward a flat Hessian assembly for a four-dimensional Regge action, a discrete model of gravity built from flat simplices. The library uses the counts to define a projection that forces a candidate second-variation form to vanish on the decoy classes. But the true per-hinge area weights and deficit kernels, the quantities that would supply numeric class weights, are not evaluated here. They remain an open target, to be derived from a Cayley–Menger calculus of dihedral angles at the flat point.

What the declaration does not claim is as important as what it proves. It does not complete the flat Hessian of the 4D Regge action. It does not prove that the discrete action converges to the Einstein–Hilbert action. It does not reverse-engineer weights from Einstein–Hilbert. The counting table is a combinatorial factor, a necessary ingredient, not the whole recipe.

/-- Total incidence mass on the seed hinge (= 2 simplices × 10 edges). -/
theorem sum_seedHingeIncidenceNat :
    (∑ d : Fin 15, seedHingeIncidenceNat d) = 20 := by
  unfold seedHingeIncidenceNat simplex0Classes simplex1Classes
  decide

/-- THEOREM: every seed-hinge boundary class has positive incidence. -/
theorem hingeBoundary_incidence_pos (i : Fin 3) :
    0 < seedHingeIncidenceNat (hingeBoundaryClass i) := by
  fin_cases i <;> decide

/-- THEOREM (decoy): three explicit edge classes have zero seed-hinge
incidence. -/
theorem seedHingeIncidence_decoy_zero :
    seedHingeIncidenceNat decoyClass4 = 0 ∧
      seedHingeIncidenceNat decoyClass8 = 0 ∧
        seedHingeIncidenceNat decoyClass12 = 0 := by
  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

What this page does not claim

The declaration does not complete the flat Hessian of the 4D Regge action. The declaration does not prove convergence to the Einstein–Hilbert action. The declaration 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/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: