CanonicalPeriodicSlotWitnessFilteredEdgeAngleSumTarget
plain-language theorem explainer
Names the flatness obligation that every positive-displacement periodic edge has total incident dihedral angle exactly 2π, summing only over cell-tets with an explicit local edge-slot witness. Gravity and Regge-calculus workers cite it as the remaining geometric input to the nonlinear Regge-to-Dirichlet continuum limit on the Freudenthal torus. The body is a pure Prop abbreviation: a universal quantifier over edges of a filtered finite sum.
Claim. For positive integers $N_x,N_y,N_z\ge 1$, the following holds: for every positive-displacement periodic edge $e$ on the $N_x\times N_y\times N_z$ torus, the sum of local Freudenthal dihedral angles over all periodic cell-tetrahedra incident to $e$ via an explicit edge-slot witness equals $2\pi$.
background
The module packages exact theorem 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 periodic edge is a base vertex together with one of seven positive cube displacements. A periodic tet is a cubic cell vertex paired with one of the six Freudenthal tetrahedron types inside that cell. The typed angle contribution of a cell-tet to an edge is the local Freudenthal dihedral angle at the recovered slot $f$ when canonicalEdgeSlot? succeeds, and the slot-witness incidence predicate is exactly the existence of such an $f$.
Filtering the finite set of all periodic tets by that witness and summing the contributions yields the classical hinge flatness condition (total angle $2\pi$) in a form that carries an explicit local edge index on every summand. That bookkeeping is what the finite incident-star classification needs.
proof idea
Definitional Prop abbreviation, not a proved theorem. The right-hand side is the universal statement that for every PeriodicEdge, the Finset sum of canonicalPeriodicTypedEdgeAngleContribution over the universe of PeriodicTet filtered by canonicalPeriodicTypedEdgeIncidentSlotWitness equals $2\pi$. No tactics or lemmas are applied; the name simply freezes that filtered angle-sum target for downstream hypotheses.
why it matters
This is the slot-witness form of the incident angle-sum (flatness) target used throughout the physical six-tet cubic Dirichlet instance. Downstream, canonicalPeriodicIncidentFilteredEdgeAngleSumTarget_of_slotWitnessFiltered shows it implies the weaker isSome-filtered target, while canonicalPeriodicSlotWitnessFilteredEdgeAngleSumTarget_of_localEdgeOfFiltered shows it is implied by the geometric localEdgeOf filtered target, so the three formulations sit in a chain.
The heavy consumer is canonicalPeriodicFullRegge_variable_weighted_finite_probe_spacing_scaled_div_spacing_norm_sq_tendsto_dirichlet_of_freudenthalRealization_slotWitnessFilteredAngleSum, whose doc-comment states the remaining flatness input as exactly this slot-witness filtered angle-sum target. That theorem is the continuum-limit bridge from the nonlinear Regge aggregate on the Freudenthal realization to Dirichlet energy. In the broader RS gravity stack it is the geometric flatness gate on the cubic lattice before continuum identification with the physical Dirichlet model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.