axisWitness_flatEdgeLengthDir_eq_explicit
plain-language theorem explainer
On the axis-witness Freudenthal cell, the general flat local edge-length directional derivative equals the specialized axis-witness formula for every local (tet, edge-slot) pair and every edge index. Gravity auditors matching the explicit fiber calculus to the audit table cite this identity. The proof unfolds both sides, rewrites vertex potentials via the tet-vertex potential lemma, and finishes by ring normalization.
Claim. For every local Freudenthal pair $(\mathrm{tet},\mathrm{slot})\in\mathrm{Fin}\,6\times\mathrm{Fin}\,6$ and every edge index $k\in\mathrm{Fin}\,6$, the flat local edge-length directional derivative of the axis-witness unit endpoint potential on the matching cell equals the specialized axis-witness flat edge-length directional value at that pair and $k$.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
A FreudenthalLocalPair is a finite table entry (tet, edge-slot) left after the periodic-cell base-offset equation is isolated. The axis-witness setup fixes lattice spacings witnessHx/Hy/Hz, a unit endpoint potential concentrated on the axis-witness edge, and an audit table axisWitnessCell that assigns an explicit matching cell to each local pair.
The left-hand side is the general flat Freudenthal local edge-length directional derivative on an encoded periodic tetrahedron, with the squared-edge factor unfolded to freudenthalTetSqEdges. The right-hand side is the specialized axis-witness formula: place the cell, read the two endpoints of edge $k$ via edgeVertices (the standard tet edge table: $0\mapsto(0,1)$, ..., $5\mapsto(2,3)$), lift them by the Freudenthal tet-vertex map, and scale by the square-root edge factor times the potential difference.
proof idea
Term-mode reduction, not a conceptual argument. Unfold both the general explicit-fiber directional derivative and the specialized axis-witness formula. Simplify with the fixed edgeVertices table so both sides name the same endpoint pair. Rewrite each endpoint potential by axisWitness_tetVertPotential_eq_xi (twice), which identifies the axis-witness unit potential on the lifted tet vertices with the explicit $\xi$ coordinates. Close with ring_nf on the resulting real arithmetic.
why it matters
Feeds directly into axisWitness_explicitPairSummand_eq_local, which equates the closed-form expanded pair summand on the explicit fiber to the local axis-witness pair summand for pairs in the displacement-0 fiber. That step is part of matching the encoded periodic Freudenthal scaffold to the physical six-tet cubic Dirichlet target: once edge-length directional pieces agree, the pair-summand and stencil-level Dirichlet actions can be compared termwise.
In the broader gravity chain this sits under the Regge cubic-lattice / Freudenthal length-chain endpoint certificates imported by the module. It is bookkeeping that makes the axis-witness audit table interchangeable with the general fiber calculus, not a new physical law. No T0–T8 forcing step is claimed here; the landmark relevance is the discrete geometric substrate used later for continuum Dirichlet limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.