LocalVertex
plain-language theorem explainer
The local vertex set of the concrete Freudenthal/cubic Regge chart is the eight-element finite type. Anyone citing the concrete area-weight matrix, second-variation coefficients, or component certificate indexes vertices by this type. The declaration is a one-line type synonym for the standard eight-point finite ordinal.
Claim. The local vertex set of the concrete flat-sector Regge model is identified with $\{0,1,\ldots,7\}$, matching the eight vertices of a cubic cell (Freudenthal local chart).
background
The module builds a fully concrete finite flat-sector Regge package that the weak-field bridge can consume without new geometric axioms. Full Cayley–Menger determinants and arbitrary dihedral derivatives are not yet exposed as differentiable maps of all edge lengths, so the comparison is proved only for a regular Freudenthal-local model whose area weights come from the regular hinge-area formula and whose second-variation data is the graph-Laplacian Regge data already used by the bridge.
In that setting a local chart has eight vertices (the vertex count of a cubic cell). Indexing those vertices by a named finite type keeps every subsequent matrix, sum, and certificate statement over a fixed discrete set rather than an abstract triangulation.
Related bookkeeping elsewhere in the stack (active-edge counts, hinge faces of glued pent complexes) is separate; here the only geometric content is the eight-vertex local chart.
proof idea
One-line type abbreviation: the local vertex type is defined to be the standard finite type with eight elements. No proof obligations.
why it matters
Every concrete object in the Freudenthal Regge component is indexed by this vertex set: the geometric area/face-weight matrix, the second-variation coefficient matrix $M_{ij}$, the off-diagonal identity $M_{ij}=-A_{ij}$, the exact zero row-sum property, and the component certificate that the second-order Regge action equals the Dirichlet form with those area weights.
The module’s honest scope is that this is the first fully concrete finite model and the exact interface a future full Cayley–Menger/dihedral derivative computation must target. Fixing eight vertices (cubic/Freudenthal chart) is the discrete skeleton of that interface; without it the Laplacian Regge data and the weak-field component comparison cannot even be stated.
It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure local discrete geometry feeding the gravity weak-field bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.