CanonicalPeriodicMixedHingeDeficitExpandedLengthChainBaseDispTypedTetTarget
plain-language theorem explainer
Defines the typed cell/tetrahedron form of the mixed hinge-deficit target on a canonical periodic Freudenthal torus of size Nx×Ny×Nz (each >2). For every vertex potential and every periodic edge, the hinge directional derivative times a base-and-displacement-filtered sum of Schläfli dihedral derivatives equals the squared potential jump scaled by edge length. Gravity workers cite it when discharging the physical six-tet Dirichlet model. The body is a pure Prop packaging, not a proved equality.
Claim. Fix lattice sizes $N_x,N_y,N_z>2$. Let $P$ be the canonical encoded periodic Freudenthal torus on that grid. The typed mixed target asserts: for every vertex potential $\xi$ and every periodic edge $e$, the hinge-measure directional derivative of $\xi$ along $e$, multiplied by the negative sum over cells and local tetrahedra whose base and displacement match $e$ of Schläfli dihedral derivatives times local edge-length directional derivatives, equals $\sqrt{|\mathrm{disp}(e)|^2}\,(\xi(v_1)-\xi(v_2))^2$.
background
The module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not free-assert the Dirichlet equality; it names the intermediate targets that must hold.
A Freudenthal triangulation splits each cube into six tetrahedra. Periodic edges carry a base vertex and a displacement; localEdgeOf maps each local tet edge slot to a global edge representative. The continuum bridge identifies a weighted graph Laplacian on vertex potentials with a hinge-area form of deficit angles: roughly $\tfrac12\sum w_{ij}(\varepsilon_i-\varepsilon_j)^2$ equals a sum of deficit times area.
The mixed target couples the hinge-measure directional derivative of a potential to an expanded length-chain of Schläfli data (dihedral derivatives times edge-length derivatives). The typed form indexes tetrahedra as cell $\times$ local tet rather than an anonymous finite index, so base/displacement filters read off the cube geometry directly.
proof idea
Definitional packaging only: the right-hand side is the squared potential jump on the edge endpoints, scaled by the Euclidean length of the periodic displacement. The left-hand side multiplies the hinge directional derivative by a double sum over PeriodicTet (cell vertex times local tet in Fin 6), retaining only those local edges whose displacement and base match the given periodic edge, then summing Schläfli dihedral derivatives against local edge-length directional derivatives. No tactics or lemmas are applied; the Prop is the obligation itself.
why it matters
This target is the typed-tet form of the base-and-displacement-filtered mixed hinge deficit on the canonical periodic torus. Downstream, canonicalPeriodicMixedHingeDeficitExpandedLengthChainBaseDispTypedTetTarget_of_cellTet lifts the cell-tet form into this typed form, and canonicalPeriodicMixedHingeDeficitExpandedLengthChainBaseDispFilteredTarget_of_typedTet pushes it onward to the filtered mixed target. The local-correspondence endpoint canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitTypedTetTargets consumes the typed mixed target (with a weighted-deficit vanishing hypothesis) to reach the canonical edge-stencil correspondence.
In the gravity stack this is one of the exact theorem obligations that close the gap between the encoded periodic Freudenthal scaffold and the physical six-tet cubic Dirichlet model. It sits on the discrete-to-continuum path that identifies Regge-style hinge deficits with a Dirichlet (graph-Laplacian) action on vertex potentials, the lattice-side avatar of the continuum bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.