freudenthalLocalPairDisp_filter_angle_sum
plain-language theorem explainer
For each of the seven positive displacement classes on the local Freudenthal table, the sum of dihedral angles over all (tet, edge-slot) pairs with that displacement equals a fixed symbolic template. Gravity and Regge-calculus workers cite it when collapsing filtered local-pair sums to closed Schläfli coefficients. The proof rewrites the filter as a fiber and applies the precomputed fiber angle-sum identity.
Claim. For every positive displacement class $d \in \{0,\ldots,6\}$, the sum of local dihedral angles over all Freudenthal local pairs $(\mathrm{tet},\mathrm{slot}) \in \{0,\ldots,5\}^{2}$ whose displacement class equals $d$ is exactly the symbolic template value assigned to $d$ (two copies each of the axis or face-diagonal slots, or six copies of the body-diagonal slot, as appropriate).
background
This module packages the 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; it isolates finite combinatorial identities that must hold before the continuum limit is taken.
After the periodic-cell base-offset equation is stripped away, what remains is a finite table of local pairs: six tetrahedra times six edge-slots. Each pair carries a positive displacement class in seven bins (three axis, three face-diagonal, one body-diagonal) and a local dihedral angle. The symbolic template for class $d$ is the closed linear combination of those angles prescribed by the Freudenthal geometry: axis classes get two copies each of slots $0,3,5$; face-diagonals get two copies each of slots $1,4$; the body-diagonal gets six copies of slot $2$.
The present statement equates the filter-sum of angles over pairs with displacement $d$ to that template. It is the filter-facing form of an equivalent fiber identity already proved in-module.
proof idea
Two-line term proof. First rewrite the filtered universe of local pairs as the displacement fiber via the equality freudenthalLocalPairDispFiber_eq_filter. Then apply the already-established fiber angle-sum lemma freudenthalLocalPairDispFiber_angle_sum, which evaluates the sum on that fiber to the symbolic template at $d$. No further arithmetic is performed here.
why it matters
Downstream, canonicalPeriodicBaseDispFilteredLocalSlotTripleSum_eq_angleTemplate uses this identity to collapse the base/displacement-filtered periodic cell/tet/slot triple sum to the symbolic local-angle template for the typed edge's displacement class. That parent theorem records the payoff: "the only remaining zero-deficit work is therefore the three explicit template identities to $2\pi$."
In the Recognition gravity stack this sits inside the Regge cubic-lattice / Freudenthal-torus bridge toward the physical six-tet Dirichlet action. Matching filtered local angles to the Schläfli template is a necessary combinatorial step before deficit angles can be shown to vanish on the flat background and before the continuum Dirichlet form is recovered. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; those enter only at the broader scaffolding that justifies the eight-tick and three-dimensional lattice geometry in which this local table lives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.