Gravity Analysis Regge Hinge4 Dflat Kernel Seed Hinge Incidence Decoy Zero

The decoy classes

The declaration seedHingeIncidence_decoy_zero is a machine-checked theorem in the Recognition Science framework's library of formal theorems. It establishes a precise combinatorial fact about a four-dimensional geometric cell built from 24 simplices, the higher-dimensional analogues of triangles. The cell is the Freudenthal-Kuhn 4-cube, a standard object in discrete geometry. Within this cell, the framework defines a specific triangle, called the seed hinge, and then counts how many of the 24 simplices contain each of the 15 possible edge types. The theorem proves that three of these 15 edge types have a count of zero: they appear in no simplex that contains the seed hinge. These three types are called decoy classes.

The proof is a direct computation, verified by the kernel of the proof assistant. It is a statement about incidence: which edges touch which simplices. The theorem also proves that the other 12 edge types do appear, and that the three boundary edges of the seed hinge itself each appear in exactly two simplices. This is the combinatorial support for a larger project: building the second variation, or Hessian, of a discrete gravity action in four dimensions. The idea is that the true physical weights for each edge type will eventually be contracted against this incidence table. The decoy classes being absent means those edge types will contribute nothing to the final sum, a structural simplification.

In Recognition Science, this is a step in a campaign to derive the Einstein-Hilbert action of general relativity from a discrete ledger of events. The framework models spacetime as a ledger, a discrete record of events, and seeks to show that its dynamics reduce to known physics. This particular theorem does not do that. It is a purely combinatorial statement about a geometric object. It does not assign any physical meaning to the decoy classes; it only proves they are absent from the incidence structure. The true per-hinge kernels, the actual physical weights, are not evaluated here and remain an open problem.

The value of this theorem is that it pins down a piece of the combinatorial skeleton on which a physical theory might be built. It is a necessary but not sufficient condition for the larger goal. It tells a researcher exactly which edge types can be ignored when assembling the Hessian for this seed hinge, saving effort and clarifying the structure. It does not, by itself, say anything about gravity in the everyday sense.

/-- 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: 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: exactly two of the 24 Freudenthal simplices contain the
seed hinge. -/
theorem seedHinge_simplex_count :
    (Finset.univ.filter (fun s : Fin 24 => containsSeedHinge s = true)).card =
      2 := by
  decide

What this page does not claim

This theorem does not assign physical meaning to the decoy classes. This theorem does not complete the flat Hessian of the 4D Regge action. This theorem does not prove that the Recognition Science action converges to the Einstein-Hilbert action.

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: