CanonicalPeriodicMixedHingeDeficitExpandedLengthChainPerEdgeTarget
plain-language theorem explainer
Packages the per-edge expanded mixed hinge-deficit identity on the canonical periodic Freudenthal torus: for every vertex potential and every edge, the hinge-measure times the summed Schläfli dihedral–length chain equals the squared potential jump scaled by edge length. Gravity and discrete-Regge workers cite it as the finite local obligation before global edge summation. It is a Prop-valued definition, not a proved equality.
Claim. Fix integers $N_x,N_y,N_z>2$ and let $P$ be the canonical encoded periodic Freudenthal torus on that lattice. The target asserts: for every vertex potential $\xi$ and every edge $e$, the product of the hinge-measure directional derivative at $e$ with the negative sum over incident tetrahedra of (dihedral-angle derivatives times local edge-length directional derivatives) equals $\sqrt{\ell_e^2}\,(\xi(v_1)-\xi(v_2))^2$, where $v_1,v_2$ are the endpoints of $e$.
background
The module ties the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not grant the Dirichlet equality for free; it packages the exact obligations needed to instantiate that model on a periodic lattice.
A Freudenthal triangulation splits each cube into six tetrahedra. Hinge measures and Schläfli data supply the first variation of deficit angles with respect to edge lengths. The mixed expanded length-chain form multiplies the hinge directional derivative by the chain-rule sum of dihedral derivatives times local length derivatives, then compares that product to the squared jump of a scalar vertex potential across the edge, scaled by Euclidean edge length.
Upstream geometry supplies edge–tet incidence, edge endpoints, and the encoded periodic complex; the dimensionless bridge ratio $K=\varphi^{1/2}$ appears in the ambient constant layer but is not the curvature functional $K(\lambda)$ of the $\lambda_{\mathrm{rec}}$ derivation.
proof idea
Definitional packaging only: bind $P$ to the canonical encoded periodic Freudenthal torus, then state a universal Prop over vertex potentials $\xi$ and edges $e$. The left-hand side is the hinge-measure directional derivative times the negative double sum (over tets incident to $e$, then over the six local edge slots) of dihedral derivatives from the triangulation Schläfli data times local edge-length directional derivatives. The right-hand side is $\sqrt{\mathrm{globalSqEdge}(e)}$ times the squared potential difference on the two endpoints of $e$. No tactics or lemmas discharge the equality.
why it matters
This is the finite local identity that remains before summing over global edges in the mixed hinge-deficit expansion. Downstream, the typed-edge form converts into this per-edge target, the per-edge target lifts to the full expanded length-chain target, and the local-correspondence endpoint theorem consumes the per-edge deficit targets (together with a weighted-deficit eventual-zero hypothesis) to reach the canonical edge-stencil correspondence.
In the Recognition gravity stack this sits inside the discrete Regge-to-Dirichlet bridge on the six-tet cubic lattice: matching the expanded hinge variation to a Dirichlet energy density edge by edge is the concrete step toward the physical six-tet cubic Dirichlet model on a periodic torus. It does not itself close continuum or continuum-limit claims; it isolates the remaining algebraic identity at edge scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.