freudenthalLocalDispMultiplicity_sum
plain-language theorem explainer
The seven local displacement-class fiber sizes on the one-cube Freudenthal edge-slot table sum to 36, equaling the count of local (tetrahedron, edge-slot) pairs. Anyone verifying that the positive displacement classes partition the 6×6 local table would cite this. The proof is a one-line native decision of a finite natural-number sum.
Claim. Let $m:\{0,\ldots,6\}\to\mathbb{N}$ be the local displacement-class multiplicities with $m(0)=m(1)=m(2)=m(6)=6$ and $m(3)=m(4)=m(5)=4$. Then $\sum_{d=0}^{6} m(d)$ equals the cardinality of the set of local Freudenthal pairs $(\mathrm{tet},\mathrm{edge\text{-}slot})\in\{0,\ldots,5\}\times\{0,\ldots,5\}$, namely $36$.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not assert the free-space Dirichlet equality; it wires the scaffold to the physical target.
After the periodic-cell base-offset equation is isolated, what remains is a finite local table of pairs: six tetrahedron types times six edge slots per tet. That table is the type of local Freudenthal pairs. Each pair carries a positive displacement class in seven bins (indices $0$ through $6$).
The multiplicity function records the fiber sizes of that classification: classes $0,1,2,6$ each have six local representatives; classes $3,4,5$ each have four. The present statement is the global count check that those fibers exhaust the $6\times 6$ table.
proof idea
Term-mode proof by native_decide. Both sides are closed natural-number expressions on finite types: the left-hand side is an explicit sum of seven hardcoded multiplicities $6+6+6+4+4+4+6$, and the right-hand side is Fintype.card of Fin 6 × Fin 6. The kernel evaluates both and confirms equality to $36$. No lemmas beyond the definitions of the multiplicity table and the local-pair abbreviation are required.
why it matters
In the gravity stack this is a bookkeeping certificate inside the physical six-tet cubic Dirichlet instance: every local (tet, edge-slot) pair must land in exactly one displacement class before hinge-aware zero-mode and stencil analyses can treat the classes as a partition. The module doc frames the file as packaging theorem obligations for the periodic Freudenthal torus model rather than claiming the continuum Dirichlet equality outright; this sum is one of those finite-table obligations.
No downstream consumers are recorded yet. The result still anchors the local edge-slot accounting that later Dirichlet-target and Hessian-is-Dirichlet siblings rely on when they assemble periodic edge stencils and mixed-axis actions. It is pure combinatorics of the Freudenthal cell, not a dynamical claim about $G$, $\phi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.