seedHinge_simplex_count
plain-language theorem explainer
Exactly two of the twenty-four Freudenthal 4-simplices of the unit 4-cube contain the seed hinge (vertex masks 0, 1, and 3). Combinatorial Regge and discrete-gravity workers cite this when fixing the seed-hinge orbit before incidence counts. The proof is a pure finite decision over the twenty-four simplices.
Claim. The number of Freudenthal 4-simplices among the $24$ axis-permutations of the unit $4$-cube whose five vertex masks include the seed hinge $\{0,1,3\}$ is exactly $2$.
background
The module enumerates the Freudenthal (Kuhn) subdivision of the unit $4$-cube: twenty-four monotone $4$-simplices, one per permutation of the four coordinate axes. Each simplex carries five nested vertices whose bitmasks record cumulative axis sums, drawn from the fifteen edge classes of the imported $4$D stencil.
The seed hinge is the triangle with vertices at masks $0$, $1$, and $3$ (origin, first basis edge, and the face spanned by the first two axes). Containment means the simplex's five vertex masks include both $1$ and $3$ (mask $0$ is automatic as the start). This sits in the QG campaign's combinatorial support layer: incidence geometry only, with per-hinge area and deficit kernels left open.
proof idea
Containment of the seed hinge is a Boolean of two decidable existentials over the five vertex masks of a simplex. Filtering the universe of twenty-four indices and taking cardinality is therefore a fully decidable finite statement. The proof is the single tactic decide, which exhausts that filter; no algebraic lemma is required.
why it matters
This is the module's seed-hinge orbit count: exactly two simplices contain the hinge, later identified as the permutations that begin with axes $(0,1)$. It underwrites the incidence-multiplicity theorems (how many seed-simplices carry each of the fifteen edge classes), the nonvacuity and axis-swap symmetry facts, and the three combinatorial decoy classes outside the support.
The flat-Hessian MODEL then contracts open per-hinge area weights against open deficit kernels, forced to vanish off this support. The count does not complete the flat Hessian of the $4$D Regge action, does not prove RS-to-Einstein–Hilbert convergence, and does not flip gap-action recovery; it only locks the combinatorial size those later steps need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.