simplexHasClass
plain-language theorem explainer
Boolean check: a Freudenthal 4-simplex (index in 0..23) carries a given edge class (among the 15 nonzero 0/1 classes) on at least one of its ten local edges. Incidence completeness theorems and the Nat class-indicator for flat-Hessian assembly cite it. The body is a decidable existential over the ten slots via the local edge-class map.
Claim. For simplex index $s\in\{0,\ldots,23\}$ and edge class $d\in\{0,\ldots,14\}$, the predicate is true if and only if there exists a local edge slot $e\in\{0,\ldots,9\}$ such that the local edge class of slot $e$ in simplex $s$ equals $d$.
background
This module enumerates the Freudenthal/Kuhn triangulation of the 4-cube: 24 monotone 4-simplices (axis permutations), each with five nested vertices and ten local edges. Edge geometry is drawn from the imported 15-class stencil of ReggeEdgeStencil4D (nonzero 0/1 masks on four axes); the module never redefines that stencil.
Each simplex-slot pair is assigned a class in $\mathrm{Fin},15$ by the local edge-class map, which subtracts one from a bounded edge mask and packages the result. The present definition asks whether a fixed class appears among those ten values for a given simplex.
The broader campaign is combinatorial support for a flat-Hessian assembly skeleton of 4D Regge gravity. Per-hinge deficit and area kernels remain OPEN parameters; this layer only tracks which classes sit on which simplices.
proof idea
Definition, not a proof. The body is decide applied to the proposition that some local edge slot $e:\mathrm{Fin},10$ has local edge class equal to $d$. Finiteness of the domain makes the existential decidable, so the result is a concrete Bool.
why it matters
This is the incidence predicate that turns the ten-slot local class table into a usable support test. Downstream, the Nat indicator classInSimplexNat is the 0/1 lift used when counting or contracting class weights. Completeness theorems for the simplex-0 and simplex-1 class tables discharge membership by reducing to this predicate and decide. The cell-wide cover theorem states every one of the 15 classes appears in some simplex, again via this check.
In the QG campaign it is deliverable-B scaffolding: combinatorial support for the MODEL flat-Hessian form that vanishes off incidence. It does not evaluate OPEN dihedral/Cayley–Menger kernels, nor close $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.