PeriodicEdgeStencilDirichletTarget
plain-language theorem explainer
Names the physical identification target that canonical incidence-weight Dirichlet energy equals the concrete periodic edge-stencil finite-difference action on an encoded Freudenthal torus. Gravity and Regge-lattice workers cite it when discharging the six-tet cubic Dirichlet model. It is a pure specialization of the general physical target to the edge-stencil action; no proof content.
Claim. For positive integers $N_x,N_y,N_z$ (each at least $3$ in the encoded data) and an encoded periodic Freudenthal torus $P$ on those sides, the proposition that for every vertex potential $\xi$ the canonical Dirichlet energy of $P$ equals the concrete edge-stencil finite-difference Dirichlet action of $P$ at $\xi$.
background
The module packages 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. An encoded periodic Freudenthal torus is a finite Triangulation3D with side lengths greater than two (ruling out degenerate wraparound) and equivalences from Fin indices to typed cells and positive-displacement edges.
The general physical target asserts that canonical Dirichlet energy from incidence weights equals a chosen concrete six-tet finite-difference action at every vertex potential. The edge-stencil candidate is the sum over encoded global periodic edges weighted by flat global edge length; it is distinct from the abstract canonical vertex-pair Dirichlet energy and is the next physical identification target.
proof idea
Definitional abbreviation only. Instantiates the general physical finite-difference Dirichlet target at the concrete periodic edge-stencil action. No tactics, no lemmas applied, no proof obligations discharged here.
why it matters
This is the named Prop that the no-self-loop discharge theorem and the canonical periodic edge-stencil theorem prove for encoded Freudenthal tori. Downstream, periodicEdgeStencilTarget_of_noSelfLoop reduces the target to a sum-commute and reindex identity once self-loops are ruled out; canonicalPeriodicEdgeStencilTarget then specializes to the canonical encoder.
It also appears in the T5-to-nonlinear-Regge J-cost bridge certificate in the unified forcing chain, linking the unique J-cost (T5) to the nonlinear Regge curvature-action side of the lattice gravity story. Closing this identification is part of making the six-tet cubic Dirichlet model a concrete physical instance rather than an abstract scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.