simplex1Classes_complete
plain-language theorem explainer
Every edge class in the simplex-1 table is realized among that simplex's ten local edges. The table is the ten-class support of Freudenthal simplex 1 (axis permutation (0,1,3,2)). Anyone checking incidence completeness for the 4D Regge hinge stencil would cite this. Proof is exhaustive Fin-case analysis plus decide.
Claim. Let $C_1 = \{0,1,2,3,7,9,10,11,13,14\} \subset \mathrm{Fin}\,15$ be the edge-class set of Freudenthal 4-simplex $1$ (axis permutation $(0,1,3,2)$). For every $d \in C_1$, simplex $1$ carries class $d$ among its ten local edges.
background
This module builds the combinatorial skeleton for the flat Hessian of the 4D Regge action on the Freudenthal/Kuhn triangulation of the 4-cube. There are 24 monotone 4-simplices (one per axis permutation) and a fixed 15-class edge stencil imported from ReggeEdgeStencil4D. Each simplex has five nested vertices and ten local edges, each edge mapped to one of the fifteen global classes.
simplexHasClass s d is the Boolean asking whether class $d$ appears among the ten local edges of simplex $s$. The set simplex1Classes is the explicit ten-element support computed for simplex $1$, the permutation $(0,1,3,2)$. The seed hinge is the triangle with vertex masks $0,1,3$; incidence multiplicities over the two seed-containing simplices are the main combinatorial deliverable of the file.
The local theoretical setting is deliverable B of the QG campaign: kernel-checked incidence and assembly scaffolding only. Per-hinge area and deficit kernels remain OPEN parameters.
proof idea
Revert the membership hypothesis so the goal is a statement over all of Fin 15 gated by membership. Then fin_cases d splits into fifteen goals. On each goal decide discharges both the membership filter and the existential ∃ e : Fin 10, localEdgeClass 1 e = d that defines simplexHasClass. No external lemmas beyond the two in-module definitions are required; the check is pure finite enumeration.
why it matters
Closes the completeness half of the simplex-1 incidence table: every listed class is actually present as a local edge, so the table is not an over-approximation. Together with the dual nonvacuity/support facts in the same module, this pins the combinatorial support that the MODEL flat-Hessian assembly is forced to vanish off of.
No downstream consumers are wired yet (used_by is empty). The result sits inside the honest scope of the module: it does not evaluate dihedral or Cayley–Menger kernels, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and does not flip gap_action_recovery. It is one of the A-shaped combinatorial gates that must hold before any numeric class-weight assembly can be trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.