CanonicalPeriodicZeroDeficitAngleSumTarget
plain-language theorem explainer
Defines the exact zero-deficit geometric obligation on a periodic Freudenthal torus: for every encoded edge, the sum of local dihedral angles from all incident tetrahedra equals 2π. Gravity and Regge-limit arguments cite it as the flatness input that turns the six-tet cubic scaffold into a physical Dirichlet model. It is a pure Prop packaging of that angle-sum condition, not a proved statement.
Claim. For positive integers $N_x,N_y,N_z$ each strictly larger than $2$, write $P$ for the canonical encoded periodic Freudenthal torus of those periods. The target asserts that for every edge index $e$ of $P$, the sum over all tetrahedra $\tau$ of the local Freudenthal dihedral angle at the oriented face (if any) by which $e$ sits in $\tau$, and $0$ otherwise, equals $2\pi$.
background
The module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not give the Dirichlet equality for free; it isolates the geometric and analytic inputs that remain.
A Freudenthal triangulation of the cube splits each cell into six tetrahedra. On the encoded periodic torus, edges and tets are finite-indexed; incidence is recorded by a partial map from (edge, tet) pairs to a local face label. The local dihedral angle of a Freudenthal tet at that face is a fixed real number coming from the Euclidean geometry of the standard Freudenthal simplex.
Zero deficit at an interior edge means the incident dihedral angles sum to a full turn $2\pi$. That is the classical Regge flatness condition. The present definition sharpens that condition to the exact incident local edge slots of the canonical encoded periodic complex, rather than an abstract typed-edge formulation.
proof idea
There is no proof: the declaration is a Prop-valued definition. It binds the canonical encoded periodic Freudenthal torus for the given periods, then states a universal quantification over finite edge indices. For each edge the body is an equality between a sum over tet indices (matching the incidence map to either a local dihedral angle or zero) and $2\pi$. Downstream lemmas discharge or transport this Prop; the definition itself only names the obligation.
why it matters
This is the sharpened flatness input that the physical six-tet cubic Dirichlet instance needs. Downstream, the typed-edge angle-sum target implies this encoded finite-index form; a companion theorem asserts the target holds on the canonical periodic torus. From it one obtains the flat local-deficit angle-sum target (after evaluating the conformal chart at zero potential), the flat-deficit zero target, and the global zero-deficit-at-flat input for the same complex.
It also appears as the remaining angle-sum hypothesis in the full nonlinear Regge finite-aggregate limit: variable-weighted probe spacing scaled by spacing-norm squared tends to Dirichlet energy once local stencil correspondence and this zero-deficit sum are supplied. In the Recognition gravity stack that closes the path from the encoded periodic Freudenthal scaffold to continuum Dirichlet energy on the cubic lattice, which is the discrete precursor to the continuum gravitational action in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.