axisWitnessSchlaefli_zero_iff
plain-language theorem explainer
If the rationalized Schläfli summand table vanishes at a local Freudenthal (tet, edge-slot) pair and direction k, the closed-form Schläfli coefficient for that pair and k is zero. Gravity and discrete-Regge auditors use it to drop vanishing axis contributions in the six-tet cubic Dirichlet packaging. Proof is a two-step rewrite: equate the closed form to the table formula, substitute the zero hypothesis, and simplify the product.
Claim. Let $\mathrm{pair}=(e,s)\in\{0,\ldots,5\}^2$ be a local Freudenthal (tet, edge-slot) pair and let $k\in\{0,\ldots,5\}$. If the rationalized Schläfli summand table entry at $(s,k)$ is zero, then the closed-form Schläfli coefficient of $\mathrm{pair}$ in direction $k$ is zero.
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; it isolates finite local data after the periodic-cell base-offset equation is removed.
A FreudenthalLocalPair is a pair in $\mathrm{Fin},6\times\mathrm{Fin},6$: a tet index and an edge-slot inside the Freudenthal cube triangulation. The closed-form Schläfli coefficient of such a pair in local direction $k$ is the dihedral closed derivative length of the corresponding Freudenthal tet edge data. Upstream, that coefficient equals the rationalized Schläfli summand table entry at the pair's edge-slot and $k$, times a positive square-root edge-length ratio:
$\mathrm{coeff}(\mathrm{pair},k)=T(s,k)\cdot\sqrt{\ell^2(k)}/(2\sqrt{\ell^2(s)})$.
The table $T$ is the evaluated rationalized Schläfli summand table at the Freudenthal squared edge lengths; many of its entries are literally zero by case analysis on $(e,k)$.
proof idea
One short tactic proof. Rewrite the closed-form coefficient via freudenthalLocalPairClosedFormSchlaefliCoeff_eq_table, which replaces it by the table entry times the positive edge-length prefactor. Substitute the hypothesis that the table entry is zero, then simp discharges $0\cdot(\cdots)=0$. No case split on the pair or on $k$ is needed once the table equality is in hand.
why it matters
In the gravity domain this lemma is a local vanishing filter for axis-witness Schläfli contributions inside the physical six-tet cubic Dirichlet instance. After the periodic Freudenthal scaffold is reduced to a finite $(tet, slot)$ table, many Schläfli summands are identically zero; this fact converts those table zeros into closed-form coefficient zeros so they drop from stencil and Hessian assemblies (siblings such as the canonical periodic edge-stencil Dirichlet target and the encoded-periodic Hessian-is-Dirichlet certificates).
It sits downstream of the Freudenthal length-chain endpoint certificate (the summand table) and the closed-form-equals-table identity. No downstream used_by edges are recorded yet; the lemma is private scaffolding for the module's Dirichlet packaging rather than a public export. Framework-wise it is pure discrete-geometry bookkeeping for Regge-type actions on the Freudenthal cube triangulation, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.