hingeBoundaryClass
plain-language theorem explainer
Enumerates the three edge classes that bound the seed hinge triangle inside the fifteen-class Freudenthal 4-cube stencil, as the identity map from three labels into the global class index. Combinatorial Regge analysts cite it when restricting incidence counts to hinge-boundary support. The body is a three-clause lookup, not a derived identity.
Claim. The hinge-boundary edge classes of the seed triangle are the three global stencil classes $0,1,2$: the map $\{0,1,2\}\to\{0,\ldots,14\}$ is $i\mapsto i$.
background
This module continues the QG full-theory campaign after the fifteen-class edge stencil of ReggeEdgeStencil4D. It enumerates the twenty-four monotone 4-simplices of a Freudenthal/Kuhn 4-cube cell and tracks which of the fifteen edge classes appear as local edges of a fixed seed hinge.
The seed hinge is the triangle with vertex masks $0$, $e_0$, $e_0+e_1$ (masks $0,1,3$). Exactly two of the twenty-four simplices contain it (permutations beginning $(0,1,\ldots)$). Its three boundary edges occupy three of the fifteen global classes; the remaining classes are either interior to the cell orbit or combinatorial decoys with zero incidence on the seed.
The present map simply names those three boundary classes so later incidence statements can quantify over them without hard-coding indices.
proof idea
Definition by exhaustive pattern match on Fin 3: each label is sent to the same natural number viewed in Fin 15. No lemmas are applied; there is no proof obligation beyond typechecking the three constructors.
why it matters
Parent theorem hingeBoundary_incidence_pos uses this map to state that every seed-hinge boundary class has strictly positive incidence (multiplicity two under the seed-simplex count). That nonvacuity fact is deliverable B of the module: combinatorial support of the flat-Hessian assembly skeleton is nonempty on the hinge boundary and forced to vanish off the incidence support.
It does not evaluate OPEN per-hinge area or deficit kernels, does not complete the flat Hessian of the 4D Regge action, and does not touch S_RS_converges_EH_4d or gap_action_recovery. Within Recognition gravity it is a small naming gate that keeps the incidence theorems index-clean before any continuum limit is attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.