canonicalPeriodicBaseDispFilteredLocalSlotTripleAngleSumTarget_holds
plain-language theorem explainer
On any positive-period Freudenthal torus, the base-and-displacement filtered triple sum of local dihedral angles over cells and six-tet slots equals the zero-deficit target for every periodic edge. Gravity and Regge-calculus workers cite it when wiring the physical six-tet cubic Dirichlet model to the encoded periodic scaffold. The proof is a one-line application of the local displacement-class angle-template identities.
Claim. For all positive integers $N_x,N_y,N_z$, the base-and-displacement filtered periodic zero-deficit target holds: for every periodic edge $e$ on the Freudenthal torus of periods $(N_x,N_y,N_z)$, the double sum over cells/tets and over the six local slots whose displacement matches $e$, of the canonical Freudenthal local dihedral angle when the base-vertex offset equation holds (else $0$), equals the zero-deficit value.
background
The module packages the exact obligations needed to instantiate PhysicalSixTetCubicDirichletModel on an encoded periodic Freudenthal torus. It does not give the physical Dirichlet equality for free; it reduces that goal to finite, checkable angle and incidence identities on the six-tet cubic triangulation.
The target here is the base-and-displacement filtered triple-sum proposition. Displacement matching is handled by a finite local-slot filter (six slots per tet, via localEdgeOf), and incidence collapses to the periodic base-vertex offset equation. The summands are the canonical Freudenthal local dihedral angles on those slots.
Upstream, the filtered target is known to follow from seven local displacement-class angle-template identities (FreudenthalLocalDispAngleTemplateTarget). Those templates encode the exact finite multiplicity table for local Freudenthal edge slots by positive displacement class.
proof idea
One-line term proof. Apply canonicalPeriodicBaseDispFilteredLocalSlotTripleAngleSumTarget_of_localDispAngleTemplates at periods $N_x,N_y,N_z$, supplying the already-established certificate freudenthalLocalDispAngleTemplateTarget as the angle-template hypothesis. That upstream lemma rewrites the filtered triple sum, edgewise, into the angle-template form and discharges the zero-deficit claim from the seven local identities.
why it matters
This is a concrete closure step in the gravity stack that links the periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model. Downstream, canonicalPeriodicDispFilteredLocalSlotTripleAngleSumTarget_holds cites it: the displacement-filtered local-slot triple target is obtained from the base-and-displacement filtered form by dropping the base-offset filter once the stronger statement is known.
In the broader Recognition framework this sits in the Regge/cubic-lattice gravity lane (Freudenthal length chain, Regge cubic lattice limit, hinge-aware zero modes). It is not a T0–T8 forcing step; it is an instance-level angle-sum identity needed so the discrete curvature/deficit bookkeeping on the eight-tick-compatible cubic triangulation matches the Dirichlet action target. Without it, the physical model cannot be instantiated on the periodic scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.