freudenthalLocalDispMultiplicity
plain-language theorem explainer
Lookup table of local fiber sizes for the seven positive displacement classes on the one-cube Freudenthal edge-slot complex: classes 0,1,2,6 each have six representatives and classes 3,4,5 each have four. Gravity and discrete-geometry workers cite it when counting local (tet, edge-slot) pairs by displacement class. It is a pure definition by cases on Fin 7.
Claim. Define a function $m : \{0,\ldots,6\} \to \mathbb{N}$ by $m(0)=m(1)=m(2)=m(6)=6$ and $m(3)=m(4)=m(5)=4$. These are the fiber sizes of the seven positive displacement classes in the one-cube Freudenthal local edge-slot table.
background
The module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it supplies the combinatorial scaffolding that later theorems discharge.
A Freudenthal triangulation of the cube yields six tetrahedra. Local edge slots are pairs (tet, edge-slot) inside one cube; there are $6 \times 6 = 36$ such pairs. Positive displacement classes index the distinct nonzero lattice displacements realized by those edges. The seven-class indexing is the discrete geometry of the cubic lattice under the Freudenthal subdivision.
This definition records, for each class $d \in \mathrm{Fin},7$, how many of the 36 local pairs realize that class. Upstream geometry (periodic Freudenthal torus, Regge cubic lattice limit, single-edge bounded complexes) supplies the ambient complex; the multiplicity table is the local counting data those constructions feed.
proof idea
Pure definition by pattern match on $\mathrm{Fin},7$. No proof obligations: each constructor is assigned a concrete natural number (six or four). Downstream positivity, sum-to-36, and fiber-cardinality theorems discharge by fin_cases plus native_decide against this table.
why it matters
The table is the combinatorial spine of the local Freudenthal displacement analysis inside the physical six-tet cubic Dirichlet instance. Three immediate parents use it: positivity of every class multiplicity, the identity that the seven multiplicities sum to the full $36$ local pairs, and the exact fiber-cardinality statement that the filtered set of local pairs of class $d$ has size $m(d)$.
Those facts underwrite the discrete Dirichlet / finite-difference action on the periodic Freudenthal torus and the passage toward the physical six-tet cubic model. In the broader Recognition gravity stack this is local lattice bookkeeping on the cubic complex that supports the Regge-action and Dirichlet-target constructions, not a forcing-chain step (T0–T8) itself. It closes a concrete counting gap so later nonnegativity and target-matching lemmas can fire without ad-hoc casework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.