freudenthalExplicitFiberClosedFormFiberSum_add
plain-language theorem explainer
The closed-form fiber sum over one positive-displacement class on the canonical periodic Freudenthal torus is additive in the vertex conformal potential. Anyone assembling mixed hinge-deficit or Dirichlet targets from these fiber sums needs this linearity. The proof unfolds the sum, distributes addition over the finite sum, and applies the pairwise expanded-summand additivity lemma.
Claim. Let $N_x,N_y,N_z\ge 3$ and let $P$ be the canonical encoded periodic Freudenthal torus of those sizes. For vertex conformal potentials $\xi,\eta$ on $P$, any positive-displacement periodic edge $e$, and any displacement class $d\in\{0,\ldots,6\}$, the closed-form fiber sum of $\xi+\eta$ along $e$ in class $d$ equals the sum of the fiber sums of $\xi$ and of $\eta$.
background
This module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus scaffold. It does not freely assert the physical Dirichlet equality; it builds the algebraic pieces that a later target can cite.
A vertex conformal potential is a real assignment to the vertices of a finite 3D triangulation. The ambient complex here is the canonical encoded periodic Freudenthal torus of sizes $N_x,N_y,N_z\ge 3$. A periodic edge is a base vertex together with one of seven positive cube displacements.
The closed-form fiber sum for one positive-displacement class aggregates expanded pair summands along the fiber of a given edge and class $d$. The sibling lemma freudenthalExplicitFiberPairClosedFormExpandedSummand_add already records that each expanded pair summand is additive in the potential; the present result lifts that to the full fiber sum.
proof idea
Term-mode, three steps. Unfold the definition of the closed-form fiber sum (a finite sum of expanded pair summands). Rewrite the goal by distributing addition over that Finset sum (sum_add_distrib). Congruence of the sum then reduces to the pairwise statement: for each pair, apply the already-proved additivity of the expanded summand under $\xi\mapsto\xi+\eta$.
why it matters
Linearity of the fiber sum is a structural prerequisite for packaging per-displacement closed-form mixed hinge-deficit targets and for equating the fiber sum to a weighted sum of vertex coefficients. Downstream, CanonicalPeriodicMixedHingeDeficitExplicitFiberClosedFormPerDispTarget needs a well-behaved closed-form fiber expression per positive-displacement class, and freudenthalExplicitFiberClosedFormFiberSum_eq_sum_vertexCoeffs rewrites the same sum in coefficient form; both cite this additivity.
In the broader gravity chain, these identities sit inside the Regge/Dirichlet correspondence on the six-tet cubic lattice limit. They are bookkeeping lemmas, not continuum gravity claims: they keep the discrete action linear in conformal potentials so that Hessian and Dirichlet targets remain quadratic forms. No T0–T8 forcing step is discharged here; the result is local to the Freudenthal scaffold packaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.