CanonicalPeriodicMixedHingeDeficitLocalAngleTarget
plain-language theorem explainer
Defines the local-angle form of the mixed hinge-deficit identity on a periodic Freudenthal torus of size Nx×Ny×Nz (each > 2). For every vertex potential, the edge sum of hinge-measure times deficit directional derivatives (from the canonical local dihedral package) must equal the edge-stencil Dirichlet energy. Gravity workers cite it as one of the exact obligations that instantiate the physical six-tet cubic Dirichlet model. It is a pure Prop packaging, not a proved equality.
Claim. Fix positive integers $N_x,N_y,N_z>2$. Let $P$ be the canonical encoded periodic Freudenthal torus of those sizes. The local-angle mixed hinge-deficit target asserts: for every vertex potential $\xi$ on $P$, $$\sum_e \bigl(\partial_{\mathrm{hinge}}\mu\bigr)(e;\xi)\,\bigl(\partial_{\mathrm{def}}\delta\bigr)_{\mathrm{loc}}(e;\xi)=E_{\mathrm{Dir}}^{\mathrm{edge}}(\xi),$$ where the deficit derivative is taken from the canonical local dihedral-angle package and $E_{\mathrm{Dir}}^{\mathrm{edge}}$ is the canonical edge-stencil Dirichlet energy.
background
The module packages exact theorem obligations that connect an encoded periodic Freudenthal torus to the physical six-tet cubic Dirichlet model. It does not free-assert the physical Dirichlet equality; it names the identities that must hold on that scaffold.
A Freudenthal triangulation of the 3-torus is cut into six tetrahedra per cube. Hinge measures and dihedral deficits live on edges; their first variations against a vertex potential $\xi$ are the directional derivatives appearing in the sum. The deficit side is specialized to the canonical local dihedral derivative package (angles assembled from incident tet slots), rather than a length-chain expansion.
The right-hand side is the canonical edge-stencil Dirichlet energy on the same complex: a discrete quadratic form built from axis displacements along the periodic lattice edges. The dimensionless bridge ratio $K=\varphi^{1/2}$ and related RS constants appear in the ambient geometry stack but do not alter the shape of this Prop.
proof idea
Definitional packaging only: bind $P$ to the canonical encoded periodic Freudenthal torus, then state a universal quantification over vertex potentials equating two real expressions (edge sum of product of hinge-measure and local-angle deficit derivatives versus edge-stencil Dirichlet energy). No tactics, no lemmas applied. Downstream lemmas convert this form to the length-chain form by unfolding the local dihedral package into an explicit localAngleLengthChainDeriv sum, and lift it to the mixed edge-stencil target.
why it matters
This Prop is one of the concrete obligations the module uses to instantiate PhysicalSixTetCubicDirichletModel on a periodic Freudenthal torus. Downstream, it is equivalent to the length-chain form of the same mixed target, implies the mixed hinge-deficit edge-stencil target, and feeds the canonical local-correspondence endpoint that expresses the mixed target as a finite local-angle identity (under a weighted-deficit eventual-zero hypothesis).
In the gravity stack this is the discrete Regge/Dirichlet bridge on the six-tet cubic lattice: matching first variations of hinge deficit against the Dirichlet energy is the finite-difference avatar of the continuum Laplace/Dirichlet action. It sits under the broader RS geometry program (periodic Freudenthal scaffold, Regge action correspondence, cubic lattice limit) rather than under the T0–T8 forcing chain itself. Closing the corresponding theorems discharges the model instance; the definition alone asserts nothing physical.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.