freudenthalExplicitFiberTablePairInnerSum_eq_flatExpandedSummand
plain-language theorem explainer
The six-slot inner sum of Schläfli dihedral derivatives times local edge-length directional derivatives, at the selected matching cell of an explicit Freudenthal fiber pair, equals the flat-unfolded per-pair summand. Regge/gravity workers instantiating the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus cite this when collapsing fiber-table sums. Proof: unfold the target summand, then termwise rewrite via the flat local edge-length derivative identity.
Claim. Let $N_x,N_y,N_z>2$, let $P$ be the canonical encoded periodic Freudenthal torus on those periods, let $\xi$ be a vertex conformal potential on $P$, let $e$ be a positive-displacement periodic edge, and let $(t,s)\in\mathrm{Fin}\,6\times\mathrm{Fin}\,6$ be a local Freudenthal (tet, edge-slot) pair. Writing $\mathrm{cell}$ for the selected matching cell of $(e,(t,s))$, $$\sum_{k\in\mathrm{Fin}\,6}\bigl(\partial\mathrm{dihedral}\,\mathrm{tetData}(P^{-1}(\mathrm{cell},t))\bigr)(s,k)\cdot(\partial_\xi\ell)(P^{-1}(\mathrm{cell},t),k)$$ equals the flat-expanded per-pair summand of $(\xi,e,(t,s))$.
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 assert the physical Dirichlet equality for free. The ambient geometry is the canonical encoded periodic Freudenthal torus $P$ on periods $N_x,N_y,N_z>2$, built from the canonical periodic endpoint incidence. A PeriodicEdge is a positive-displacement edge given by a base vertex and one of seven cube displacements. Vertex conformal potentials are real functions on the finite vertex set of a 3D triangulation.
Local Freudenthal pairs are the finite table $\mathrm{Fin},6\times\mathrm{Fin},6$ of (tet, edge-slot) indices left after the periodic-cell base-offset equation is isolated. The Schläfli data of the triangulation supply dihedral derivatives at each tet and slot; the local edge-length directional derivative is $\sqrt{a_f},(\eta(u)+\eta(v))/2$ along a conformal potential $\eta$. The left-hand side here is the inner slot sum of those two factors at the selected matching cell; the right-hand side is the already flat-unfolded per-pair summand used by the stencil/Dirichlet packaging.
proof idea
One short tactic proof. Unfold the definition of the flat-expanded per-pair summand, then apply Finset.sum_congr with a reflexive index equality. On each summand $k\in\mathrm{Fin},6$, rewrite the local edge-length directional derivative factor by the upstream identity freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv_eq at the selected matching cell, the pair's tet index, and slot $k$. No further algebraic manipulation is required: after that rewrite the two sides match definitionally.
why it matters
In the gravity domain this is a bookkeeping bridge inside the physical six-tet cubic Dirichlet instance: it certifies that the explicit-fiber table's Schläfli $\times$ edge-length inner sum, evaluated at the selected matching cell, is identical to the flat-unfolded per-pair summand that the Dirichlet/stencil targets consume. The module's job is to connect the encoded periodic Freudenthal torus scaffold to PhysicalSixTetCubicDirichletModel by discharging such exact equalities rather than asserting the physical Dirichlet law outright.
Sibling packaging (canonical Hessian-is-Dirichlet, periodic edge-stencil Dirichlet action and targets, mixed-axis stencil action) sits in the same file; this lemma is the fiber-table half of that collapse. No downstream used_by edges are recorded yet, so it is presently a leaf obligation inside the instance. Framework-wise it lives in the Regge/cubic-lattice gravity layer (periodic Freudenthal geometry, first variation, Hessian), not in the T0–T8 forcing chain, but it is part of making the discrete gravitational action on the eight-tick-compatible cubic scaffold fully explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.