freudenthalLocalPairLengthChainSummand
plain-language theorem explainer
Defines the local length-chain summand for one Freudenthal (tet, edge-slot) pair as the dot product of closed-form Schläfli coefficients with six edge-length directional derivatives. Gravity and Regge-calculus workers cite it when assembling the symbolic Dirichlet length chain on the six-tet cubic cell. The body is a one-line finite sum, not a derived identity.
Claim. For a local Freudenthal pair $p = (\mathrm{tet},\mathrm{slot}) \in \{0,\ldots,5\}^2$ and a map $\ell' : \{0,\ldots,5\} \to \mathbb{R}$ of edge-length directional derivatives, the local length-chain summand is $\sum_{k=0}^{5} c_{p,k}\,\ell'(k)$, where $c_{p,k}$ is the closed-form Schläfli coefficient of $p$ in direction $k$.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not freely assert the physical Dirichlet equality; it isolates finite local data after the periodic-cell base-offset equation is removed.
A Freudenthal local pair is an element of $\mathrm{Fin},6 \times \mathrm{Fin},6$: one tetrahedron index and one edge-slot index in the six-tet cubic triangulation. The closed-form Schläfli coefficient of such a pair in local direction $k$ is the dihedral closed length-derivative of the Freudenthal tetrahedron at that slot and direction. The six edge-length directional derivatives are the conformal variations the caller supplies per local edge slot.
The summand is the elementary building block of the local length-chain: each pair contributes a linear form in those six derivatives, ready to be summed over displacement fibers.
proof idea
Pure definitional abbreviation. The body is the finite sum $\sum_{k:\mathrm{Fin},6} c(p,k),\ell'(k)$ with $c$ the closed-form Schläfli coefficient. No tactics or lemmas; downstream equalities such as the coeff-dot form and the expanded-summand identity are rfl against this definition.
why it matters
Feeds the local displacement length-chain sum template (sum of this summand over the positive-displacement fiber) and the explicit-fiber template used on the periodic torus. Equality theorems identify it with the expanded closed-form summand and with the plain coefficient dot product, so later Dirichlet and Hessian arguments can rewrite freely between those presentations.
In the broader gravity stack this is the local Schläfli contribution that must match the physical finite-difference Dirichlet target on the six-tet cubic cell. It sits inside the Regge-action / periodic Freudenthal scaffold path toward the physical model instance, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.