freudenthalExplicitFiberDispLengthChainSumTemplate
plain-language theorem explainer
Defines the explicit-fiber length-chain sum for a periodic Freudenthal edge: sum over local pairs in a displacement fiber of the length-chain summand built from flat edge-length directional derivatives at each pair's selected cell. Gravity and Regge-calculus workers cite it when matching closed-form fiber sums to stencil Dirichlet data. The body is a direct Finset sum over the fiber with the directional-derivative template plugged in.
Claim. For lattice sizes $N_x,N_y,N_z>2$, a vertex conformal potential $\xi$ on the canonical encoded periodic Freudenthal torus, a positive-displacement periodic edge $e$, and a fiber index $d\in\{0,\ldots,6\}$, the template value is $\sum_{p\in F(d)} S(p;\,k\mapsto \partial_{\ell_k}\ell^{\mathrm{flat}}(\xi;\,c(e,p),t(p)))$, where $F(d)$ is the local-pair displacement fiber, $S$ is the length-chain summand, and $c(e,p)$ is the selected periodic cell for pair $p$ on edge $e$.
background
The module packages theorem obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not freely assert the physical Dirichlet equality; it builds the exact scaffolding needed to connect the torus geometry to that target.
A periodic edge is a base vertex plus one of seven positive cube displacements. Vertex potentials are real assignments on the triangulation vertices. The flat local edge-length directional derivative evaluates, on an encoded periodic tetrahedron, the derivative of edge length in the conformal direction with squared-edge factors unfolded to the Freudenthal tet edge squares.
The length-chain summand for a local pair is the closed-form Schläfli-coefficient dot product against a six-component edge-length derivative vector. The displacement fiber indexes which local pairs contribute for a given displacement class $d$.
proof idea
Pure definitional construction, not a proof. Sum over freudenthalLocalPairDispFiber d. For each pair, feed freudenthalLocalPairLengthChainSummand the map that sends edge index $k$ to the flat local edge-length directional derivative of $\xi$ at the cell selected by freudenthalExplicitFiberPairSelectedCell for that edge and pair, on the pair's tet and edge $k$. No lemmas are applied; the expression is the template itself.
why it matters
Feeds the equality freudenthalExplicitFiberClosedFormFiberSum_eq_disp_lengthChainTemplate, which identifies the closed-form fiber sum with this template evaluated at the edge's own displacement. Also sits under freudenthalLocalPairLengthChainSummand_eq_coeffDot, the rfl identity that the length-chain summand is the Schläfli-coefficient dot product.
In the Recognition gravity stack this is the explicit bridge between fiberwise Regge length variation on the periodic Freudenthal scaffold and the finite-difference Dirichlet stencil targets used for the physical six-tet cubic model. It is definitional scaffolding inside the Gravity domain, not a forcing-chain (T0–T8) step, but it is required before any claim that the encoded torus realizes the physical Dirichlet action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.