freudenthalLocalPairClosedFormExpandedSummand_add
plain-language theorem explainer
The closed-form Schläfli/length-chain summand on one local Freudenthal (tet, edge-slot) pair is additive in the six conformal edge-length directional derivatives. Anyone assembling the physical six-tet cubic Dirichlet action from fiberwise pair contributions needs this linearity. The proof unfolds the finite sum and distributes addition through the sum and the coefficient multiplications.
Claim. Let a local Freudenthal pair be an element of $\mathrm{Fin}\,6\times\mathrm{Fin}\,6$ (tet index and edge-slot). For any two maps $f,g:\mathrm{Fin}\,6\to\mathbb{R}$ of conformal edge-length directional derivatives, the closed-form expanded summand of the pair on $f+g$ equals the sum of the summands on $f$ and on $g$.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it connects the encoded periodic Freudenthal scaffold to that target.
A local Freudenthal pair is the finite table left after the periodic-cell base-offset equation is isolated: an element of $\mathrm{Fin},6\times\mathrm{Fin},6$ indexing a tet and an edge-slot. The closed-form expanded summand for one such pair is the Schläfli/length-chain contribution $$\sum_{k\in\mathrm{Fin},6} D_{\mathrm{dih}}(\mathrm{freudenthalTet},\mathrm{slot},k),\partial_k\ell,$$ with caller-supplied conformal edge-length directional derivatives $\partial_k\ell$ and fixed dihedral closed-derivative length coefficients on the Freudenthal cube triangulation.
Additivity in those six directional inputs is the elementary algebraic property needed before summing pairs into a global Dirichlet-type action.
proof idea
Unfold the definition of the expanded summand to a finite sum over $\mathrm{Fin},6$. Rewrite via Finset.sum_add_distrib so the sum of the two summands becomes a single sum of pointwise sums. Congruence of sums reduces to the $k$-th summand: pointwise addition on $\mathrm{Fin},6\to\mathbb{R}$ (Pi.add_apply) and left-distributivity of real multiplication (mul_add) give
$$c_k,(f+g)(k)=c_k f(k)+c_k g(k)$$
with $c_k$ the fixed dihedral coefficient. No geometric input is used beyond the sum shape.
why it matters
In the gravity stack, the physical six-tet cubic Dirichlet instance is built from local Freudenthal pair contributions on the periodic cell. Linearity of each closed-form summand in the edge-length directional derivatives lets the total action split cleanly under superposition of conformal variations, which is the natural algebraic step toward Hessian/Dirichlet quadratic forms (cf. sibling targets such as the canonical Hessian-is-Dirichlet and periodic edge-stencil Dirichlet action packages).
No downstream theorem currently cites this lemma in the graph, so it is infrastructure inside the pair-level closed-form layer rather than a named paper proposition. It sits under the broader program that ties the encoded periodic Freudenthal torus and Regge/length-chain geometry to a physical Dirichlet model; it does not itself force $D=3$, the eight-tick octave, or the J-cost uniqueness chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.