canonicalPeriodicMixedHingeDeficitExpandedLengthChainExplicitFiberTarget_of_typedEndpoint
plain-language theorem explainer
On a periodic Freudenthal torus of size at least 3 in each direction, the typed-endpoint form of the expanded mixed hinge-deficit length-chain identity implies the explicit table-fiber form that expands the incident sum over the precomputed local pair-displacement fiber. Gravity workers discharging six-tet cubic Dirichlet obligations on the encoded torus cite this bridge. The proof rewrites the fiber sum by the Freudenthal expanded-sum table lemma, negates, and transports the typed hypothesis.
Claim. Let $N_x,N_y,N_z\ge 3$. If the mixed hinge-deficit expanded length-chain identity holds in typed-endpoint form on the canonical encoded periodic Freudenthal torus of size $(N_x,N_y,N_z)$ (RHS written from the typed periodic edge displacement and endpoints), then it holds in explicit table-fiber form: the same left-hand side equals a sum over the precomputed local pair-displacement fiber of that edge's displacement, with each summand the Schläfli dihedral derivative times the local edge-length directional derivative on the matched base cell.
background
This module does not assert the physical Dirichlet equality outright. It packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus scaffold.
Two sibling targets appear. The typed-endpoint target states the mixed identity for every vertex potential $\xi$ and every periodic edge, with the right-hand side written from the typed edge displacement and endpoints (hinge-measure directional derivative times a negated incidence sum over tetrahedra matching the edge). The explicit-fiber target replaces that incidence sum by a sum over the precomputed local pair-displacement fiber for the edge's displacement class, routing each pair through a periodic matching base cell and the triangulation Schläfli data.
Upstream geometry supplies the incidence map from global edges into local tet edge slots, the encoded torus with its edge and tet equivalences, and the expanded-sum comparison between the fiber table and the typed edge-in-tet incident sum.
proof idea
Fix the canonical encoded periodic Freudenthal torus $P$. For arbitrary potential $\xi$ and periodic edge, pull the abstract edge $e$ back along $P$'s edge equivalence.
Invoke the upstream equality that the explicit fiber-table expanded sum equals the typed edge-in-tet expanded incident sum. A Finset.sum_congr step unfolds the explicit fiber pair summand definition so the table matches the selected-cell form. Compose to identify the fiber inner sum with the typed incident sum, then negate both sides.
Specialize the typed-endpoint hypothesis at $(\xi,\mathrm{edge})$ and rewrite the negated fiber identity into that equation. A final simpa closes the explicit-fiber target.
why it matters
The declaration is a pure target-form bridge inside the physical six-tet cubic Dirichlet instance stack: it lets later arguments work with the precomputed fiber table while hypotheses are stated in the cleaner typed-endpoint language.
Its sole recorded consumer is the axis-displacement-0 witness theorem that the typed-endpoint target fails on a concrete unit witness lattice. That negative result uses the conversion (or its context) when discharging the typed assumption toward a contradiction, so the bridge is load-bearing for both positive packaging and concrete falsification checks of candidate length-chain identities.
In the broader gravity program this sits among the Regge/Freudenthal lattice-limit obligations that connect discrete hinge deficits to continuum Dirichlet-type actions; it does not itself touch the T0–T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.