freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv_eq
plain-language theorem explainer
On the canonical encoded periodic Freudenthal torus, the abstract local edge-length directional derivative at a tetrahedron equals the explicit fiber flat closed form, cell by cell and edge index by edge index. Gravity and Regge-lattice workers cite it when unfolding Schläfli-type sums on the six-tet cubic model. The proof simp-unfolds both sides and rewrites via the flat squared-edge identity.
Claim. Fix lattice sizes $N_x,N_y,N_z>2$, a vertex potential $\xi$ on the canonical encoded periodic Freudenthal torus $P$, a cell $c$, a tetrahedron index $t\in\{0,\ldots,5\}$, and a local edge index $k\in\{0,\ldots,5\}$. Then the local edge-length directional derivative of $\xi$ on $P$ at the tetrahedron corresponding to $(c,t)$ in direction $k$ equals the explicit Freudenthal-fiber flat formula at $(c,t,k)$.
background
The module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not free-assert the physical Dirichlet equality; it connects the encoded periodic Freudenthal scaffold to that target.
A Freudenthal decomposition splits each cubic cell into six tetrahedra. The canonical encoded periodic Freudenthal torus $P$ carries a tetrahedron equivalence tetEquiv identifying abstract tets with cell-index pairs, and a discrete length calculus on edges. The local edge-length directional derivative measures how a chosen edge length of a tet responds to a vertex-potential variation $\xi$.
At canonical periodic flatness, squared edge lengths admit a closed Freudenthal form. The companion explicit-fiber map evaluates that flat table directly from $(N_x,N_y,N_z)$, $\xi$, cell, tet, and edge index, without routing through the abstract torus encoding.
proof idea
One short tactic proof. Bind $P$ as the canonical encoded periodic Freudenthal torus. Goal is equality of localEdgeLengthDirectionalDeriv at P.tetEquiv.symm (cell, tet) with the explicit-fiber flat map. Unfold both definitions by simp only. The remaining obligation is the squared-edge identity at flatness, discharged by rewriting canonicalPeriodicFlat_tet_sqEdge_eq_freudenthal at the same cell, tet, and edge index.
why it matters
This bridge lets every later sum that needs edge-length derivatives work in the explicit fiber coordinates rather than the abstract torus encoding. Downstream it feeds freudenthalExplicitFiberPairFlatExpandedSummand_eq_expanded and freudenthalExplicitFiberTablePairInnerSum_eq_flatExpandedSummand. The latter states that the explicit-fiber table inner slot sum (Schläfli times local edge-length derivative) matches the flat-unfolded per-pair summand at the selected matching cell.
In the Recognition gravity stack this is scaffolding closure for the physical six-tet cubic Dirichlet instance: once directional derivatives are identified with the closed Freudenthal table, pair sums and stencil actions can be compared to the finite-difference Dirichlet target on the periodic lattice. It sits under the Regge cubic-lattice limit and nonlinear correspondence imports, not under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.