freudenthalLocalDispMultiplicity_pos
plain-language theorem explainer
Every one of the seven local Freudenthal displacement classes has strictly positive fiber size in the one-cube edge-slot table (six or four representatives). Gravity workers packaging the six-tet cubic Dirichlet model on a periodic Freudenthal torus cite this to guarantee no empty class. The proof is exhaustive case split on Fin 7 discharged by native decision.
Claim. For every displacement class $d \in \{0,1,\ldots,6\}$, the local Freudenthal edge-slot multiplicity $m(d)$ satisfies $0 < m(d)$. Explicitly $m(0)=m(1)=m(2)=m(6)=6$ and $m(3)=m(4)=m(5)=4$.
background
The module packages exact theorem obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not freely assert the physical Dirichlet equality; it wires the scaffold to the model target.
The local multiplicity function assigns to each of seven displacement classes the number of representatives among the one-cube Freudenthal edge slots: classes $0,1,2,6$ each have six local representatives, and classes $3,4,5$ each have four. Those seven fiber sizes sum to the full $6 \times 6 = 36$ local (tet, edge-slot) pairs.
Upstream, the multiplicity table is the concrete lookup used here; the surrounding geometry imports supply the periodic Freudenthal torus and Regge cubic-lattice limit infrastructure against which the Dirichlet target is stated.
proof idea
Tactic proof by exhaustive case analysis: fin_cases splits the argument over the seven values of Fin 7, and each residual goal is closed by native_decide against the closed-form multiplicity table (six or four). No algebraic lemmas are required beyond the definitional values.
why it matters
Positivity of every displacement-class fiber is a bookkeeping gate in the physical six-tet cubic Dirichlet packaging: empty classes would break the accounting that the seven multiplicities cover all thirty-six local Freudenthal (tet, edge-slot) pairs. The module's role is to connect the encoded periodic Freudenthal torus scaffold to the physical Dirichlet model target without smuggling the equality as free data.
No downstream consumers are recorded yet, so this sits as a local positivity certificate inside the gravity Dirichlet instance layer rather than a named step of the T0–T8 forcing chain. It supports the discrete geometric side of the RS gravity story (Regge-type cubic lattice, Freudenthal length chain) once the remaining instance obligations are discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.