simplex_class_count
plain-language theorem explainer
Every Freudenthal 4-simplex in the unit 4-cube carries exactly ten of the fifteen nonzero 0/1 edge classes. Gravity analysts assembling the 4D Regge flat Hessian cite this as the fixed per-cell edge budget on the combinatorial support. The proof is exhaustive case analysis over the twenty-four simplices, closed by decidable arithmetic on the class indicators.
Claim. For every Freudenthal 4-simplex $s$ among the $24$ monotone simplices of the unit 4-cube, $\sum_{d} \mathbf{1}_{s}(d) = 10$, where the sum runs over the $15$ nonzero $0/1$ edge classes and $\mathbf{1}_{s}(d)\in\{0,1\}$ is $1$ precisely when class $d$ appears as a local edge of $s$.
background
The module builds the combinatorial skeleton for the 4D Regge flat Hessian on the Freudenthal (Kuhn) triangulation of the unit 4-cube. That cell decomposes into $24$ monotone 4-simplices, one per permutation of the four coordinate axes. Edge geometry is never redefined here: the $15$ nonzero $0/1$ edge classes are imported from the 4D edge stencil.
Each simplex is recorded by five nested vertices and the masks of the edges they span. The indicator classInSimplexNat s d is $1$ when class $d$ appears among those local edges of simplex $s$, and $0$ otherwise. Summing the indicator over all fifteen classes therefore counts how many distinct stencil classes the simplex actually carries.
A 4-simplex has $\binom{5}{2}=10$ edges, so the count ten is the geometric expectation once each local edge is identified with a unique nonzero class mask. The theorem makes that identification global and kernel-checked for every cell.
proof idea
Term-mode proof by exhaustive case split: fin_cases s opens one goal per element of Fin 24. On each concrete simplex the sum of fifteen Nat indicators is a closed numeric expression, and decide evaluates it to $10$. No intermediate lemmas are invoked beyond the definition of the class indicator (itself a thin wrapper around the boolean simplexHasClass).
why it matters
This is item 1 of the module's honest deliverable B: explicit enumeration of the $24$ Freudenthal simplices together with their ten edge-class masks among the fifteen stencil classes. It pins the per-cell edge budget that later incidence counts (seed-hinge orbit, multiplicity tables, decoy classes) rely on combinatorially.
In the broader QG campaign it sits one kernel-checked increment after the 4D edge stencil. It does not evaluate per-hinge area or deficit kernels, does not assemble the numeric flat Hessian, and does not touch S_RS_converges_EH_4d or gap_action_recovery. It only certifies that the combinatorial support of each simplex is exactly ten classes, so the MODEL assembly formula knows the right contraction dimension before any OPEN weight is supplied.
No downstream theorem yet consumes it (used_by is empty); it is infrastructure for the incidence and nonvacuity block in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.