seedHingeIncidenceNat_values
plain-language theorem explainer
Closed-form incidence multiplicities of all 15 Regge edge classes on the seed hinge of the Freudenthal 4-cube cell. Combinatorial gravity and Regge-calculus workers cite the table when fixing the support of the flat Hessian class form. The proof is a single finite decidability check against the two seed-containing simplices.
Claim. Let $I(d)$ be the number of seed-containing 4-simplices in which edge class $d\in\{0,\ldots,14\}$ appears as a local edge. Then $I=(2,2,2,2,0,1,1,2,0,1,1,2,0,2,2)$: classes $0$--$3$, $7$, $11$, $13$, $14$ have multiplicity $2$; classes $5,6,9,10$ have multiplicity $1$; classes $4,8,12$ are absent.
background
The module builds the combinatorial skeleton of a 4D Regge flat Hessian on the Freudenthal/Kuhn triangulation of the unit 4-cube. Twenty-four monotone 4-simplices arise as axis permutations; each carries ten local edges among the fifteen global edge classes of the imported stencil.
The seed hinge is the triangle with vertex masks $0$, $e_0$, $e_0+e_1$. Exactly two of the twenty-four simplices contain it (those whose axis order begins $(0,1,\ldots)$). The incidence function under study counts, for each class $d$, how many of those two simplices list $d$ among their local edges: it is the sum of two indicator memberships, hence valued in ${0,1,2}$.
Module scope is deliberately narrow: incidence support and an assembly skeleton that contracts open per-hinge area and deficit kernels, forced to vanish off that support. Numeric dihedral/Cayley–Menger weights remain open parameters.
proof idea
One-line decidability proof. Both sides of each equality are closed natural-number terms built from finite membership tests on the two fixed seed-simplex class lists, so decide discharges the fifteen-way conjunction with no lemmas and no arithmetic rewriting.
why it matters
Fills item 3 of the module's honest deliverable list: explicit incidence multiplicities on the seed hinge orbit. Together with the nonvacuity, axis-swap symmetry, and decoy facts in the same file, it pins the combinatorial support that the MODEL flat-Hessian class form is allowed to touch.
It does not evaluate open per-hinge kernels, does not complete the flat Hessian of the 4D Regge action, and does not flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D. No downstream theorems currently consume it; it is a kernel-checked table for later assembly lemmas. In the broader RS gravity campaign it is a support gate after the 15-class edge stencil, not a dynamics or mass-ladder result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.