freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv_add
plain-language theorem explainer
On the encoded periodic Freudenthal torus, the flat local edge-length directional derivative is additive in the pair of conformal vertex potentials. Discrete-gravity and Regge analysts cite it when lifting single-edge linearity to pair summands. The proof unfolds the explicit formula, applies pointwise addition of potentials, and finishes by ring.
Claim. Let $N_x,N_y,N_z>2$ and let $\xi,\eta$ be real conformal potentials on the vertices of the canonical encoded periodic Freudenthal torus of those sizes. For every cell, every local tetrahedron index in the six-tet decomposition, and every local edge index $k\in\{0,\ldots,5\}$, the flat local edge-length directional derivative of $\xi+\eta$ equals the sum of the derivatives of $\xi$ and of $\eta$.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not freely assert the physical Dirichlet equality. Vertices are the periodic cubic lattice $V=\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. A vertex potential is a real function on the triangulation's vertex set (conformal degrees of freedom in the 3D Regge Hessian).
The ambient geometry is the canonical encoded periodic Freudenthal torus built from the endpoint-incidence scaffold. The object under study is the directional derivative of the flat (undeformed) local edge length along a chosen fiber edge inside one of the six tetrahedra of a cubic cell. Additivity of that scalar in the potential is the elementary linearity step before summing over pairs and edges.
proof idea
One short tactic proof. simp only unfolds the explicit definition of the flat local edge-length directional derivative and rewrites the sum of potentials pointwise via Pi.add_apply. The resulting expression is bilinear (differences of potential values on edge endpoints), so ring closes the equality.
why it matters
Feeds the immediate parent freudenthalExplicitFiberPairFlatExpandedSummand_add, which lifts single-edge additivity to the expanded pair summand used in the six-tet fiber assembly. That chain is part of the obligation package connecting the encoded periodic Freudenthal torus to the physical six-tet cubic Dirichlet target (finite-difference Dirichlet action on the cubic lattice). In the broader RS gravity stack this is bookkeeping for the discrete conformal Hessian / Regge side, not a new continuum claim: it keeps the linear structure of edge-length variations intact so later nonnegativity and stencil-target theorems can treat sums of potentials without extra error terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.