freudenthalLocalDispLengthChainSumTemplate
plain-language theorem explainer
Symbolic local length-chain sum over the explicit Freudenthal local-pair fiber for one positive displacement class. Callers feed one conformal edge-length directional derivative per local edge slot. Gravity workers wiring the six-tet cubic Dirichlet model on the periodic Freudenthal torus cite this template. It is a plain Finset sum of the per-pair Schläfli-weighted length-chain summands.
Claim. For each positive displacement class $d\in\{0,\ldots,6\}$ and each map of conformal edge-length directional derivatives $\ell':\{0,\ldots,5\}\to\mathbb{R}$, the local length-chain sum is $\sum_{(t,e)\in F_d}\sum_{k=0}^{5} c_{(t,e),k}\,\ell'(k)$, where $F_d$ is the explicit local Freudenthal (tetrahedron, edge-slot) fiber of $d$ and $c_{(t,e),k}$ are the closed-form Schläfli coefficients of that pair.
background
The module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not free the physical Dirichlet equality; it only supplies the algebraic scaffolding needed to specialize that target.
A positive displacement class is an index in $\mathrm{Fin},7$. For each class $d$, the local-pair displacement fiber $F_d$ is an explicit finite set of Freudenthal local pairs (tetrahedron type, edge slot). Each pair carries a closed-form Schläfli coefficient vector; the per-pair length-chain summand is the inner product of that vector with the six conformal edge-length directional derivatives supplied by the caller.
The length primitive from the recognition calculus is the discrete length of a finite trace; here the same idea appears as a weighted sum of edge-length derivatives along the local fiber, not as a path length on the torus itself.
proof idea
Definition, not a proof. The body is the Finset sum of the per-pair length-chain summand over the explicit local-pair displacement fiber of $d$. Each summand expands as $\sum_{k},c_{\mathrm{pair},k},\ell'(k)$ with closed-form Schläfli coefficients. No tactics or lemmas are applied at this site; equality theorems downstream recover the sum by rfl or by rewriting the fiber as a filter of the universe.
why it matters
This template is the named right-hand side for the exact local length-chain identities on the six-tet cubic Dirichlet instance. Downstream, the fiber-sum theorem states that summing the summands over the explicit fiber equals the template (proved by rfl), and the filter-sum theorem equates the same template to the sum over the computable filter of pairs with displacement $d$.
Those identities sit inside the bridge from the encoded periodic Freudenthal torus to the physical six-tet cubic Dirichlet model. They keep the conformal edge-length directional data symbolic, so later specialization (including the explicit periodic fiber template named in the doc-comment) can plug in concrete derivatives without re-deriving the local sum structure. In the broader gravity stack this is bookkeeping for Regge-style hinge and edge contributions on the cubic lattice limit, not a claim about continuum Einstein equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.