CanonicalPeriodicMixedHingeDeficitExpandedLengthChainBaseDispCellTetTarget
plain-language theorem explainer
Defines the mixed hinge-deficit target on the canonical periodic Freudenthal torus with the tetrahedron sum factored as an explicit cell sum times a local six-tet sum. Gravity workers cite it when discharging the physical six-tet cubic Dirichlet model via cell/tet product form rather than typed PeriodicTet. It is a pure Prop packaging of an edgewise identity; no proof content.
Claim. For lattice sizes $N_x,N_y,N_z\ge 3$, let $P$ be the canonical encoded periodic Freudenthal torus. The target asserts: for every vertex potential $\xi$ and every periodic edge $e$, the hinge-measure directional derivative of $\xi$ along $e$, times the negative sum over cells and local tetrahedra of the matching dihedral-derivative/length-derivative contributions (selected when the edge base and displacement match the translated local cube edge), equals $\sqrt{|\mathrm{disp}(e)|^2}\,(\xi(u)-\xi(v))^2$ at the endpoints of $e$.
background
The module packages exact theorem obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
The scaffold is the canonical encoded periodic Freudenthal torus $P$ on an $N_x\times N_y\times N_z$ lattice with each side at least 3. Edges are periodic edges with base vertex and displacement; local cube edges come from the Freudenthal six-tet triangulation via localEdgeOf. Vertex potentials $\xi$ live on the discrete vertex set of $P$.
The mixed target equates a hinge-measure directional derivative times a Schläfli-style sum of dihedral derivatives against length derivatives, to a finite-difference Dirichlet stencil $\sqrt{|\mathrm{disp}|^2}(\Delta\xi)^2$. This definition is the product-split form: the sum over typed periodic tetrahedra is written as $\sum_{\mathrm{cell}}\sum_{\mathrm{tet}\in\mathrm{Fin},6}$ rather than a single sum over $\mathrm{Vertex}\times\mathrm{Fin},6$.
proof idea
Definition only: the body is the Prop obtained by specializing the mixed hinge-deficit expanded length-chain identity to $P:=$ the canonical encoded periodic Freudenthal torus, then expanding the typed-tet sum into an explicit double sum over cells and local tetrahedra, with incidence filters on base vertex (via addVertexBits and cube-edge base) and displacement (via cubeEdgeDisp and localEdgeOf). No tactics or lemmas are applied.
why it matters
This Prop is the cell/tet product form of the mixed target used to close local-correspondence endpoints for the physical six-tet cubic Dirichlet instance. Downstream, canonicalPeriodicMixedHingeDeficitExpandedLengthChainBaseDispTypedTetTarget_of_cellTet lifts it to the typed-tet form, and ..._of_localPair discharges it from a local-pair hypothesis. Two correspondence theorems then consume the cell-tet targets: one under weighted-deficit eventual-zero input, one under the weaker weighted-stationary Schläfli input, both aiming at canonical periodic edge-stencil local correspondence.
In the broader RS gravity stack this sits on the Regge/Freudenthal discrete curvature side that feeds continuum Dirichlet limits, not on the T0–T8 forcing chain directly. It is scaffolding for the physical model instance rather than a closed continuum theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.