freudenthalExplicitFiberPairClosedFormExpandedSummand_add
plain-language theorem explainer
The closed-form expanded summand for one local Freudenthal (tet, edge-slot) pair is additive in the vertex conformal potentials. Anyone assembling fiber sums or Dirichlet actions on the canonical encoded periodic Freudenthal torus cites this. The proof rewrites each side to the flat expanded summand, then applies the already-proved flat additivity lemma.
Claim. Let $N_x,N_y,N_z>2$ and let $\xi,\eta$ be vertex conformal potentials on the canonical encoded periodic Freudenthal torus of those sizes. For any positive-displacement periodic edge and any local Freudenthal pair $(\mathrm{tet},\mathrm{slot})\in\{0,\ldots,5\}^2$, the closed-form explicit-fiber expanded summand of $\xi+\eta$ equals the sum of the summands of $\xi$ and of $\eta$.
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.
A local Freudenthal pair is an element of $\mathrm{Fin},6\times\mathrm{Fin},6$: a tetrahedron index together with an edge-slot inside the six-tet cubic cell, after the periodic-cell base-offset equation has been isolated. Vertex potentials are real functions on the vertices of the triangulation $K$ of the canonical encoded periodic Freudenthal torus. A periodic edge is a base vertex plus one of seven positive cube displacements.
The closed-form explicit-fiber expanded summand is the real contribution of one such pair at one edge for a given potential. An upstream flat version of the same summand already has an additivity lemma; a sibling equality identifies the closed-form summand with that flat expression.
proof idea
Term-mode proof in two layers. First rewrite the left-hand side and both right-hand summands via the equality that identifies the closed-form expanded summand with its flat counterpart (applied once to $\xi+\eta$, once to $\xi$, once to $\eta$). The goal collapses to additivity of the flat expanded summand, which is discharged by the existing flat additivity lemma on the same lattice sizes, potentials, edge, and local pair.
why it matters
Additivity at the pair-summand level is the inductive step for additivity of the closed-form fiber sum over local pairs. The sole recorded consumer is the fiber-sum additivity theorem in the same module, which lifts this identity from one pair to the full fiber sum at a fixed displacement class.
That fiber-sum additivity is part of the obligation package connecting the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet target (finite-difference Dirichlet action and Hessian/Dirichlet correspondence on the cubic lattice). In the broader gravity chain this supports linearity of the discrete action in conformal potentials before continuum or Regge limits are taken. It does not itself close the physical Dirichlet equality; it only supplies the algebraic additivity brick those parent theorems need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.