CanonicalPeriodicMixedHingeDeficitExpandedLengthChainExplicitFiberTarget
plain-language theorem explainer
Explicit fiber form of the mixed hinge-deficit expanded length-chain target on the canonical periodic Freudenthal torus. For every vertex potential and periodic edge, the hinge-measure directional derivative times a signed Schläfli sum over the precomputed local-pair displacement fiber equals edge length times the squared potential jump. Gravity workers cite it when wiring the physical six-tet cubic Dirichlet instance. The declaration is a Prop package, not a proved equality.
Claim. For $N_x,N_y,N_z>2$, let $P$ be the canonical encoded periodic Freudenthal torus on that lattice. The target asserts: for every vertex potential $\xi$ and every periodic edge $e$, $$\partial_{\mathrm{hinge}}(\xi,e)\cdot\Bigl(-\sum_{p\in F(d_e)}\sum_{k=0}^{5} D^{\mathrm{dih}}_{p,k}\,\partial_{\ell_k}\xi\Bigr)=\sqrt{|d_e|^2}\,(\xi(v_1)-\xi(v_2))^2,$$ where $F(d_e)$ is the precomputed Freudenthal local-pair displacement fiber for the edge displacement $d_e$, and the inner data come from the triangulation Schläfli incidence of $P$.
background
This module links the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. It does not give the physical Dirichlet equality for free; it packages the exact obligations needed to instantiate that model on a periodic torus.
The ambient geometry is the canonical encoded periodic Freudenthal torus $P$ on an $N_x\times N_y\times N_z$ lattice with each side strictly larger than 2. Edges are typed periodic edges; each carries a displacement whose squared length is periodicDispSqEdge. Local tetrahedral edge slots map to global one-cube representatives via localEdgeOf and a cube-edge base vertex, then to a matching base cell on the torus.
The left-hand side mixes a hinge-measure directional derivative in the vertex potential $\xi$ with a double sum: over the precomputed local-pair displacement fiber of the edge, and over the six local edge slots of each incident tet, weighting Schläfli dihedral derivatives by local edge-length directional derivatives. The right-hand side is the continuum-style Dirichlet stencil term: geometric edge length times $(\Delta\xi)^2$.
proof idea
Definitional Prop, not a proved theorem. The body binds $P$ to the canonical encoded periodic Freudenthal torus, then states a universal equality over vertex potentials $\xi$ and periodic edges. For each edge it pulls the abstract edge via the torus edge equivalence, multiplies the hinge-measure directional derivative by the negated fiber sum (pairs from the precomputed displacement fiber, cells from periodic matching of the cube-edge base, Schläfli tet data and local length derivatives), and equates that product to $\sqrt{\mathrm{disp}^2},(\Delta\xi)^2$. No tactics or lemmas are applied; downstream theorems discharge or transport this Prop.
why it matters
This is the explicit table-fiber obligation used throughout the physical six-tet cubic Dirichlet instance. Downstream results treat it as the hub form: it is equivalent to the flat-unfolded fiber target; it follows from the angle-chain, typed-endpoint, and flat-unfolded variants; and it implies the angle-chain form and the local-pair fiber target. The local-correspondence endpoint theorem that feeds the weighted-deficit stationary target also consumes this explicit-fiber package.
In the broader Recognition gravity stack, the goal is to realize the physical finite-difference Dirichlet action on the periodic Freudenthal triangulation (six tets per cube) so that the discrete hinge/Regge side matches the continuum stencil. Packaging the mixed hinge-deficit length-chain identity with a concrete fiber table makes that match checkable edge-by-edge without re-deriving incidence combinatorics at each use site. It does not itself close the Dirichlet equality; it is the precise Prop those closing theorems quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.