axisWitnessFlatEdgeLengthDir
plain-language theorem explainer
Defines the axis-witness directional edge-length contribution on a local Freudenthal (tet, edge-slot) pair: reference edge length times the average of the two endpoint axis potentials. Gravity and Regge-calculus workers cite it when assembling the closed-form Schläfli summands for the physical six-tet cubic Dirichlet model. The body is a pure arithmetic expression over the Freudenthal edge table and torus vertex lifts.
Claim. For a local Freudenthal pair $(\tau,s)\in\{0,\ldots,5\}^2$ and edge index $k\in\{0,\ldots,5\}$, let $C$ be the axis-witness cell of the pair, let $(u,v)$ be the two vertices of edge $k$ in tetrahedron $\tau$, and lift them by the cell offset to torus vertices $V_0,V_1$. The value is $\sqrt{q_k}\cdot(\xi(V_0)+\xi(V_1))/2$, where $q_k\in\{1,2,3\}$ is the squared Freudenthal reference length of edge $k$ and $\xi$ is the axis-witness endpoint potential.
background
The module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
A local Freudenthal pair is a finite table entry $(\tau,s)\in\mathrm{Fin},6\times\mathrm{Fin},6$ left after the periodic-cell base-offset equation is isolated. Each unit cube is split into six Freudenthal tetrahedra (tetVerts), with six edges per tet whose squared lengths are the fixed tuple $(1,2,3,1,2,3)$: three unit steps, two face diagonals, one body diagonal. Edge index $k$ maps to a vertex pair in $\mathrm{Fin},4$ via the standard tet edge table (edge 0 = (0,1), ..., edge 5 = (2,3)).
Torus vertices are obtained by adding the eight cube-corner bit offsets of a local vertex to a base cell (addVertexBits). The axis-witness cell and endpoint potential $\xi$ are the fixed witness data of this module against which directional edge-length derivatives are evaluated.
proof idea
Pure definition, no proof obligations. Unpack the axis-witness cell of the pair; read the two local tet vertices of edge $k$ from the Freudenthal edge table; lift both by addVertexBits into the periodic torus; return $\sqrt{q_k}$ times the arithmetic mean of the two endpoint $\xi$ values. Downstream lemmas unfold this expression with dsimp and discharge the edge-table lookups by simp.
why it matters
This is the edge-level building block of the axis-witness Schläfli sum. The pair summand is exactly $\sum_k c_{\tau,s}(k)\cdot$ (this quantity), and the closed-form evaluations axisWitnessPairSummand_00, _10, _23, _35, etc., reduce those sums to concrete rationals such as $-1/2$ and $-1$. The equality lemma axisWitness_flatEdgeLengthDir_eq_explicit identifies it with the general freudenthal explicit-fiber flat local edge-length directional derivative, so the witness sits inside the same Regge calculus pipeline used for the physical Dirichlet target.
In the broader Recognition gravity stack this feeds the periodic Freudenthal torus scaffold toward the cubic Dirichlet model (finite-difference Hessian matching), which is the discrete geometric side of the continuum limit rather than a T0–T8 forcing step. It closes no open physical claim by itself; it supplies the arithmetic spine those summand lemmas need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.