freudenthalExplicitFiberFlatLocalEdgeLengthDirectionalDeriv_selectedCell5
plain-language theorem explainer
On the N=5 periodic lattice, the flat local edge-length directional derivative at the selected explicit-fiber cell equals the geometric tet-edge scale times the average of the two endpoint potentials in typed vertex coordinates. The mixed LHS slot expansion cites this to cancel square roots against coefficient atoms. The proof rewrites the selected cell, unfolds the derivative, and matches both endpoints to canonical tet vertices.
Claim. Let $\xi$ be a vertex potential on the $N=5$ periodic cubic lattice, $e$ a periodic edge, $p$ a Freudenthal local pair, and $k\in\{0,\ldots,5\}$ a tet-edge index. At the selected explicit-fiber cell for $(e,p)$, the flat local edge-length directional derivative along edge $k$ of the first tet of $p$ equals $\sqrt{s_k}\,(\xi(v_0)+\xi(v_1))/2$, where $s_k$ is the squared Freudenthal tet edge length for index $k$ and $v_0,v_1$ are the two endpoints of that edge in the selected cell's bit-offset coordinates.
background
This module certifies the corrected Freudenthal axis-stencil residual on the $N=5$ periodic lattice by exact rational arithmetic (no floats). It audits every unordered monomial $\xi(u)\xi(v)$ in the mixed explicit-fiber residual, mirroring the Python endpoint analysis script.
The ambient geometry is the Freudenthal cube triangulation used by the 3D Regge Hessian: each local pair supplies a pair of tets, and each of the six tet edges carries a squared length $s_k$ from the standard Freudenthal edge table. Vertex potentials live on the $N=5$ periodic vertex set (VertexPotential5); edges are PeriodicEdge objects on the $5\times5\times5$ torus.
The selected cell is the canonical explicit-fiber representative of a local pair relative to a periodic edge. The flat local edge-length directional derivative is the first variation of edge length in the flat (undeformed metric) background, evaluated at that cell. Coefficient atoms later expand the residual in the same typed vertex coordinates, so this identity is the bridge between the geometric derivative and the monomial bookkeeping.
proof idea
Tactic proof in four steps. First rewrite the selected cell via selectedCell5_eq_freudenthalExplicitFiberPairSelectedCell, aligning the $N=5$ helper with the generic explicit-fiber selected-cell construction. Unfold the flat local edge-length directional derivative and the $N=5$ potential-at-vertex abbreviation, then dsimp. Apply freudenthalExplicitFiber_canonicalTetVerts_eq twice (once per endpoint of edgeVertices k), each time discharging the three decidable side conditions by decide. Both endpoints then sit in the bit-offset form used by the coefficient atoms, and the right-hand side is definitionally the geometric scale times the averaged potentials.
why it matters
Parent consumer is explicitFiberMixedLhsSlot_scaledPairExpansionAtN5: one real explicit-fiber Schläfli/local-length slot equals the corresponding scaled coefficient atom after edge/pair square-root cancellation. That expansion needs the derivative already written in the same typed coordinates as the atoms; this lemma supplies exactly that rewrite for the selected cell.
In the broader gravity stack this is bookkeeping inside the corrected Freudenthal axis-stencil certificate, not a new physical law. It keeps the residual audit exact and coordinate-consistent so every monomial coefficient can be checked rationally. Framework landmarks (T0–T8, RCL, $\varphi$-ladder) are upstream of the Regge/Freudenthal geometry and are not invoked here; the lemma is local to the $N=5$ stencil residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.