freudenthalExplicitFiberPairClosedFormExpandedSummand
plain-language theorem explainer
Defines the closed-form expanded real summand for one local Freudenthal (tet, edge-slot) pair on the canonical periodic torus, built from flat local edge-length directional derivatives of a vertex potential. Gravity and Regge-lattice workers cite it when assembling explicit-fiber hinge-deficit expansions. The body selects the pair's cell and feeds the six directional derivatives into the local closed-form pair expansion.
Claim. For lattice sizes $N_x,N_y,N_z>2$, a vertex potential $\xi$ on the canonical encoded periodic Freudenthal torus, a positive-displacement periodic edge, and a local pair $(\mathrm{tet},\mathrm{slot})\in\{0,\ldots,5\}^2$, return the real closed-form expanded summand obtained by evaluating the local pair closed-form expansion on the six flat local edge-length directional derivatives of $\xi$ at the pair's selected cell.
background
The module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not freely assert the physical Dirichlet equality. The geometric substrate is the canonical encoded periodic Freudenthal torus on $N_x\times N_y\times N_z$ with each side larger than 2. A periodic edge is a base vertex plus one of seven positive cube displacements. A local Freudenthal pair is a finite table entry in $\mathrm{Fin},6\times\mathrm{Fin},6$ after the periodic-cell base-offset equation is isolated: one tetrahedron index and one edge-slot index.
Vertex potentials live on the torus vertex set (with dimensionless bridge ratio $K=\varphi^{1/2}$ appearing in the encoded complex). Upstream, flat local edge-length directional derivatives supply the first-variation data that enter Regge-style hinge measures. The closed-form local pair expansion is the algebraic object that turns those six directional numbers into a single real summand for mixed hinge-deficit bookkeeping.
proof idea
Definitional, not a proof. Select the cell associated to the given periodic edge and local pair via freudenthalExplicitFiberPairSelectedCell. Pass that cell's six flat local edge-length directional derivatives of $\xi$ (indexed by the pair's tet component) into freudenthalLocalPairClosedFormExpandedSummand. The result is the closed-form expanded real contribution of that single local pair.
why it matters
This summand is the per-pair atom of the closed-form explicit-fiber mixed hinge-deficit target: that target quantifies over potentials and edges and sums these summands fiberwise. Downstream bridges equate the closed-form target with the flat-unfolded target, and the axis-witness lemma identifies the summand with a concrete local axis pair contribution. Coefficient certificates expand one explicit-fiber local pair into six checked endpoint-slot atoms using the same family of summands. In the broader RS gravity stack this sits inside the Regge cubic-lattice / six-tet Dirichlet instantiation that links discrete hinge action on the Freudenthal scaffold to continuum Dirichlet energy, feeding the physical model obligations rather than a free continuum claim. It is scaffolding glue on the path from encoded periodic geometry to certified stencil coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.