CanonicalPeriodicMixedHingeDeficitExpandedLengthChainTarget
plain-language theorem explainer
Fully expanded finite-sum form of the mixed hinge-deficit target on the canonical periodic Freudenthal torus: for every vertex potential, the edge-sum of hinge-measure derivatives times nested Schläfli dihedral and local edge-length derivatives equals the canonical edge-stencil Dirichlet energy. Discrete-gravity workers cite it when wiring the six-tet cubic Dirichlet model. Pure Prop packaging; no proof content.
Claim. For $N_x,N_y,N_z>2$, let $P$ be the canonical encoded periodic Freudenthal torus on those sizes. The claim is that for every vertex potential $\xi$ on $P$, $$\sum_e m'_e(\xi)\Bigl(-\sum_\tau\sum_{k=0}^{5} \partial_\theta\,\ell'_k\Bigr)=E_{\mathrm{Dir}}(\xi),$$ where $m'_e$ is the hinge-measure directional derivative, the inner sum runs over tetrahedra incident to edge $e$ with Schläfli dihedral derivatives and conformal local edge-length derivatives, and $E_{\mathrm{Dir}}$ is the canonical edge-stencil Dirichlet energy.
background
The module packages theorem obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not give the physical Dirichlet equality for free; it only records the exact identities needed to connect the scaffold to that model.
A Freudenthal triangulation of the 3-torus decomposes each cube into six tetrahedra. Hinge deficits and dihedral angles enter through the Schläfli identity: the first variation of volume couples edge-length changes to dihedral derivatives. The mixed hinge-deficit target expands that variation into an explicit finite sum over global edges, incident tets, and the six local edges of each tet, using conformal local edge-length directional derivatives of a vertex potential $\xi$.
The right-hand side is the canonical edge-stencil Dirichlet energy on the same complex: a discrete quadratic form built from the periodic edge stencil. Equality of the two sides is the local correspondence that later feeds the physical model.
proof idea
Definitional Prop, not a proved theorem. The body binds $P$ to the canonical encoded periodic Freudenthal torus for the given lattice sizes, then states a universal quantification over vertex potentials $\xi$: the fully expanded double-sum form of the mixed hinge-deficit directional derivative (hinge-measure factor times nested sums over tets and six local edges of Schläfli dihedral derivatives times local edge-length derivatives) equals the canonical edge-stencil Dirichlet energy of $\xi$. No tactics or lemmas are applied; the equality is the content of the proposition.
why it matters
This expanded target is the finite local identity that remains before (or after) summing over global edges in the six-tet cubic Dirichlet pipeline. Downstream, canonicalPeriodicMixedHingeDeficitExpandedLengthChainTarget_of_perEdge lifts the per-edge form to this global sum, and canonicalPeriodicMixedHingeDeficitLengthChainTarget_of_expanded collapses the expanded form back to the shorter length-chain target. The local-correspondence endpoint theorem then uses the expanded target to certify that the canonical edge stencil matches the mixed deficit derivative on the periodic Freudenthal torus.
In the broader Recognition gravity stack this sits under the discrete Regge/Dirichlet correspondence on the $D=3$ eight-tick geometry forced by the unified chain (T7–T8). It is scaffolding for the physical model instance, not a closed continuum limit or a curvature-forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.