canonicalPeriodicIncidenceConsistent
plain-language theorem explainer
Packages a witness that the canonical periodic Freudenthal triangulation on an Nx×Ny×Nz three-torus is incidence-consistent. Gravity and discrete-Regge analysts cite it whenever the canonical Regge Hessian, Dirichlet edge energy, or seven-class stencil identity is instantiated. The body is a one-line application of the endpoint-incidence constructor to the canonical endpoint data.
Claim. For positive integers $N_x,N_y,N_z$, the canonical periodic Freudenthal triangulation of the $N_x\times N_y\times N_z$ three-torus is incidence-consistent: its edge-slot incidence data form a global partition of the kind required by the nonlinear Regge first-variation theorem.
background
The module builds a typed periodic Freudenthal torus: vertices, positive-displacement edges, and tetrahedra on a three-torus, without yet fixing a concrete finite Fin-indexing. The goal is that any finite Triangulation3D encoding of this model carry a global incidence edge-slot partition, the combinatorial hypothesis of the nonlinear Regge first-variation theorem.
Incidence consistency is that partition package: every edge appears in the right dual slots with coherent endpoint data, so squared edge lengths and Hessian dual weights are well-defined globally. The canonical periodic triangulation is the standard Freudenthal subdivision of the cubic lattice, wrapped periodically in each coordinate; nonzero side lengths rule out degenerate $+1=-1$ wraparound.
Downstream stencil work treats this witness as the fixed combinatorial background on which vertex potentials, global squared edge lengths, and the Regge Hessian are evaluated.
proof idea
One-line wrapper. It applies the general constructor that builds incidence consistency from endpoint incidence data, feeding the canonical periodic endpoint-incidence certificate for sides $N_x,N_y,N_z$. No extra case splits or arithmetic; the work lives in those two named ingredients.
why it matters
This is the combinatorial handle almost every stage-1 Freudenthal stencil identity threads through. Parent results include equality of the canonical edge-stencil Dirichlet energy with the seven-class stencil energy; transport of global squared edge lengths to periodic displacement squares; equality of the frozen Hessian quadratic form with the seven-class stencil sum; the panel-locked identity $\rho(N),Q_N(u)=h^3\sum_x\sum_d c_d((u(x+d)-u(x))/h)^2$ for $N>2$; and the $\rho(N)$-normalized scaled canonical energy used when sampling continuum fields.
Regge TT-symbol preflight also freezes identifications against this same witness. In the broader Recognition geometry stack it sits under the $D=3$ spatial setting (forcing chain T8) as the discrete 3-torus mesh on which continuum limits of the Regge Hessian are compared to stencil operators. It does not close the finite-encoder obligation named in the module doc; it only certifies incidence once the canonical triangulation object is already in hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.