freudenthalLocalPairDispFiber_eq_filter
plain-language theorem explainer
For each of the seven positive displacement classes, the hand-written local Freudenthal fiber table equals the set of all (tet, edge-slot) pairs whose computed displacement is that class. Gravity and Regge-lattice authors cite it to swap explicit fibers for filter-based sums. The proof is exhaustive case analysis on Fin 7 discharged by native_decide.
Claim. For every displacement class $d \in \{0,\ldots,6\}$, the explicit fiber set of local Freudenthal pairs of class $d$ equals the filter of all pairs $(t,e)\in\{0,\ldots,5\}^2$ whose positive displacement class equals $d$.
background
The module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not claim the physical Dirichlet equality for free; it isolates finite combinatorial tables left after the periodic-cell base-offset equation is removed.
A local Freudenthal pair is a pair $(t,e)\in\mathrm{Fin},6\times\mathrm{Fin},6$: one of six tetrahedra in the cube triangulation and one of six edge slots on that tet. The positive displacement class of such a pair is the $\mathrm{Fin},7$ value of the cube-edge displacement of the corresponding local edge. The explicit fiber table lists, for each class $d$, the pairs that realize it (classes $0,1,2,6$ have six representatives; $3,4,5$ have four). The filter form is the definitional membership predicate obtained by scanning the full $6\times 6$ table.
proof idea
Term-mode proof by exhaustive case split on the displacement index $d:\mathrm{Fin},7$. Each of the seven goals is a pure finite-set equality between a concrete Finset literal and a filtered universe; native_decide closes every case by kernel computation. No algebraic lemmas are invoked.
why it matters
This equality is the bridge between the hand-curated fiber table and every sum written over the computable filter. Downstream, the axis-stencil certificate rewrites membership in the fiber to equality of displacements; the local-angle and length-chain sum theorems replace filter sums by the explicit fiber templates; the expanded mixed-hinge and explicit-fiber sum identities inherit the same rewrite. In the Recognition gravity stack this is scaffolding for the physical six-tet cubic Dirichlet instance on the periodic Freudenthal torus, feeding the Regge cubic-lattice limit and hinge-deficit length-chain targets rather than a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.