freudenthalExplicitFiberClosedFormVertexCoeff
plain-language theorem explainer
Coordinate-basis coefficient of the explicit-fiber closed-form sum at one vertex, for a fixed positive-displacement periodic edge and cube displacement class. Lattice gravity and Regge-action workers cite it when expanding the fiber sum as a linear form on vertex potentials. The definition is the fiber sum evaluated on the unit spike at that vertex.
Claim. For lattice sizes $N_x,N_y,N_z>2$, a positive-displacement periodic edge $e$, a displacement class $d\in\{0,\ldots,6\}$, and a vertex index $i$ on the canonical encoded periodic Freudenthal torus, the coefficient is the closed-form fiber sum of the unit vertex potential concentrated at $i$ (and zero elsewhere).
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 free-assert the physical Dirichlet equality; it only assembles the theorem-shaped targets that make that instantiation possible.
A periodic edge is a base vertex together with one of the seven positive cube displacements. The closed-form fiber sum takes a real vertex potential on the canonical encoded torus and returns a scalar for one fixed positive displacement class. The present coefficient is that sum evaluated on the standard basis potential that is $1$ at a single vertex index and $0$ elsewhere, so it is the coordinate of the fiber sum as a linear form on vertex potentials.
proof idea
One-line definitional wrapper. It applies the closed-form fiber sum to the standard basis potential Pi.single i 1 (unit mass at vertex index $i$), holding the lattice bounds, edge, and displacement class fixed. No further algebraic reduction.
why it matters
The coefficient is the building block for the linear expansion of the fiber sum. Downstream, the equality theorem states that the closed-form fiber sum of an arbitrary potential equals the sum over vertices of coefficient times potential value; a companion lemma records scalar homogeneity. Those facts discharge the vertex-coefficient expansion target used when wiring the periodic Freudenthal scaffold into the physical six-tet cubic Dirichlet model.
In the broader gravity stack this sits under the Regge cubic-lattice and Freudenthal length-chain imports: it turns an abstract fiber sum into an explicit stencil coefficient on the seven positive cube displacements, which is what a Dirichlet-type discrete action needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.