freudenthalLocalPairClosedFormExpandedSummand
plain-language theorem explainer
Closed-form Schläfli length-chain summand for one local Freudenthal (tet, edge-slot) pair: a linear form that pairs the six closed-form edge-length derivatives of a dihedral angle on the unit-cube Freudenthal tetrahedron against caller-supplied conformal edge-length directions. Gravity and Regge-calculus workers cite it when expanding hinge-measure first variations on the six-tet cubic lattice. The body is a pure finite sum, not a proved identity.
Claim. For a local Freudenthal pair $(\tau,e)\in\{0,\ldots,5\}^2$ and a map $L':\{0,\ldots,5\}\to\mathbb{R}$ of conformal edge-length directional derivatives, define $$S(\tau,e;L')=\sum_{k=0}^{5}\Bigl(\frac{\partial\theta_e}{\partial L_k}\Bigr)_{T_{\mathrm{Fr}}}\,L'(k),$$ where $T_{\mathrm{Fr}}$ is the unit-cube Freudenthal tetrahedron and $\partial\theta_e/\partial L_k$ is the closed-form conversion of the squared-edge dihedral derivative to an edge-length derivative.
background
The module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it isolates the finite local data left after the periodic-cell base-offset equation is removed.
A local Freudenthal pair is an element of $\mathrm{Fin},6\times\mathrm{Fin},6$: a tetrahedron index together with an edge-slot on that tet. The geometric backbone is the unit-cube Freudenthal tetrahedron $T_{\mathrm{Fr}}$, a nondegenerate tet whose squared edge lengths are the standard Freudenthal pattern.
Upstream, dihedralClosedDerivLength converts a squared-edge derivative of a dihedral angle into an edge-length derivative by the chain rule factor $2L_k=2\sqrt{\mathrm{sqEdge}(k)}$, under the local smoothness hypotheses for the cofactor angle. The present definition feeds those six coefficients against an arbitrary directional map on edge lengths, producing one Schläfli/length-chain summand.
proof idea
Definition only: expand as the finite sum over the six edge slots $k$ of the product of the closed-form edge-length dihedral derivative of the unit-cube Freudenthal tet at the pair's edge-slot against the caller-supplied directional value at $k$. No tactics, no lemmas applied beyond the referenced coefficient map. Downstream equality to the length-chain summand is definitional (rfl).
why it matters
This is the local atomic summand used throughout the six-tet cubic Dirichlet instance. Downstream it is identified with the length-chain summand, shown additive in the directional map, and lifted to the explicit-fiber closed-form expanded summand on the periodic torus. Axis-witness comparisons and the scaled pair expansion at $N=5$ in the axis-stencil coefficient certificate both expand hinge-measure directional derivatives through this form.
In the broader Recognition gravity stack it sits on the Regge side of the correspondence: Schläfli variations of dihedral angles against edge-length directions are the discrete curvature response that must match the physical finite-difference Dirichlet action on the cubic lattice. It does not close the physical equality; it supplies the exact local building block those obligations quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.