freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv
plain-language theorem explainer
Defines the flat local edge-length directional derivative on one Freudenthal tetrahedron of an encoded periodic torus: square root of the fixed squared edge length times the average vertex potential at the two endpoints. Gravity and Regge-stencil authors cite it when expanding first-variation length chains and axis-stencil coefficients. The body is a pure closed-form definition, not a proof.
Claim. Fix lattice sizes $N_x,N_y,N_z>2$, a vertex potential $\xi$ on the canonical encoded periodic Freudenthal torus, a cell, a tetrahedron index $t\in\{0,\ldots,5\}$, and an edge index $k\in\{0,\ldots,5\}$. The value is $\sqrt{s_k}\,(\xi(v_1)+\xi(v_2))/2$, where $s_k\in\{1,2,3\}$ is the $k$-th Freudenthal squared edge length (unit step, face diagonal, or body diagonal) and $v_1,v_2$ are the two endpoints of edge $k$ in that tetrahedron.
background
The module packages exact 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 supplies the geometric ingredients those obligations need.
A Freudenthal triangulation splits each unit cube into six tetrahedra. Every such tetrahedron has the same local squared-edge tuple: three unit steps ($s=1$), two face diagonals ($s=2$), and one body diagonal ($s=3$). The canonical encoded periodic torus identifies cells and tetrahedra with a global tet index via an equivalence, and exposes tet-vertex maps into the torus vertex set.
A vertex potential is a real assignment on those vertices. In the flat (zero-curvature) regime the first variation of edge length reduces to the geometric length scale times the average potential on the two endpoints; this definition writes that quantity with the squared-edge factor unfolded explicitly.
proof idea
Definition only, no tactic proof. Bind the canonical encoded periodic torus $P$, invert the tet equivalence to recover the global tetrahedron $\tau$ from the cell and local tet index, and read the two local edge endpoints from the standard edge-vertex table at index $k$. Return $\sqrt{\texttt{freudenthalTetSqEdges}(k)}$ times the arithmetic mean of $\xi$ at the two image vertices under $P$'s tet-vertex map. The square-root factor is therefore the fixed Freudenthal edge length $\sqrt{1}$, $\sqrt{2}$, or $\sqrt{3}$.
why it matters
This is the explicit flat length-derivative atom used throughout the physical six-tet Dirichlet instance. Downstream, the length-chain sum template evaluates it at each fiber entry's selected periodic cell; additivity, homogeneity, and equality lemmas rewrite sums and scalar multiples of these atoms. Axis-witness lemmas identify it with the witness flat edge-length derivative, and the axis-stencil coefficient certificates expand mixed left-hand sides into checked endpoint-slot atoms after square-root cancellation against Schläfli coefficients.
In the broader Recognition gravity stack this sits inside the Regge-calculus bridge from the periodic Freudenthal scaffold to a discrete Dirichlet (finite-difference) action. It is scaffolding for the first-variation / hinge-measure side of that bridge, not a claim about continuum GR or the forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.