axisWitness_explicitPairSummand_eq_local
plain-language theorem explainer
On the axis witness (unit endpoint potential, base edge along e_x, displacement class 0), the closed-form explicit-fiber expanded summand of any local Freudenthal (tet, edge-slot) pair equals the purely local pair summand built from Schläfli coefficients times flat edge-length directional derivatives. Gravity/Regge lattice workers cite it when collapsing the global fiber formula to a cell-local stencil. The proof unfolds definitions, substitutes the unique selected cell, and matches each summand via the flat-length directional identity.
Claim. Let a local Freudenthal pair $p=(t,s)\in\mathrm{Fin}\,6\times\mathrm{Fin}\,6$ lie in the displacement-$0$ fiber. On the axis witness (periodic edge with base $(1,0,0)$ and displacement $0$, and the corresponding unit endpoint vertex potential), the closed-form explicit-fiber expanded summand of $p$ equals $\sum_{k=0}^{5} c_{p,k}\,\partial_{\ell_k}^{\mathrm{flat}}\xi$, where $c_{p,k}$ are the local closed-form Schläfli coefficients and the derivatives are the axis-witness flat edge-length directional derivatives of $p$.
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 $(t,s)\in\mathrm{Fin},6\times\mathrm{Fin},6$ left after the periodic-cell base-offset equation is isolated. The displacement-$0$ fiber collects those pairs whose matching base cell sits on the chosen axis witness edge (base $(1,0,0)$, disp $0$). The axis-witness endpoint unit potential is the vertex potential that is $1$ on the two endpoints of that edge and $0$ elsewhere.
Upstream, axisWitness_selectedCell_eq identifies the explicit-fiber selected cell with the local axis-witness cell for every pair in the fiber, and axisWitness_flatEdgeLengthDir_eq_explicit equates the explicit-fiber flat edge-length directional derivative at that cell with the local axis-witness derivative. The local pair summand is the finite sum of Schläfli coefficients times those local derivatives; the explicit-fiber expanded summand is the corresponding global closed-form expression before specialization.
proof idea
Term-mode proof by definitional reduction and two rewrites. Unfold the explicit-fiber expanded summand, the local axis-witness pair summand, and the intermediate local closed-form expanded summand. Rewrite the selected cell via axisWitness_selectedCell_eq (using membership in the disp-$0$ fiber). The remaining equality is a sum over $k:\mathrm{Fin},6$; apply Finset.sum_congr, unfold the Schläfli coefficient, and finish each summand by axisWitness_flatEdgeLengthDir_eq_explicit.
why it matters
This is the per-pair bridge from the global explicit-fiber closed form down to the local axis-witness stencil on displacement class $0$. The sole downstream consumer is FreudenthalAxisDisp0AllPairExplicitSummandsEqLocalTarget_holds, which simply quantifies the same identity over the whole fiber and thereby discharges the axis-disp-$0$ half of the all-pairs explicit-summands target.
In the broader gravity stack, that target is part of packaging the physical six-tet cubic Dirichlet model on the periodic Freudenthal torus (Regge cubic lattice limit / Freudenthal length-chain endpoint certificates). Matching expanded summands to local Schläfli-weighted flat derivatives is the algebraic step that lets the discrete Dirichlet action be read off cell by cell rather than from the full encoded torus potential. No T0–T8 forcing step is claimed here; the result is lattice-geometry bookkeeping inside the gravity instantiation path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.