canonicalPeriodicReggeAction_zeroPotential_eq_zero_of_flatConfiguration
plain-language theorem explainer
On the canonical encoded periodic Freudenthal torus with lattice sizes greater than 2, any flat configuration makes the Regge action of the zero potential vanish. Gravity and continuum-limit arguments cite this as the exact flat-action normalization. The proof is a one-line term that converts flat configuration into a flat-deficit target and applies the zero-deficit vanishing lemma.
Claim. Let $N_x,N_y,N_z\ge 3$. On the canonical encoded periodic Freudenthal torus of those sizes, if the edge-length data form a flat configuration, then the Regge action evaluated at the zero potential is exactly $0$.
background
This module packages the theorem 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; it supplies the exact flat-action and correspondence data the continuum pipeline consumes.
A flat configuration means the discrete edge lengths realize zero curvature in the Regge sense on the encoded torus complex. The zero potential is the trivial assignment of edge potentials. The Regge action is the nonlinear discrete gravitational action built from deficit angles and dual volumes on that complex.
The lattice-size hypotheses $N_x,N_y,N_z>2$ ensure the periodic Freudenthal encoding has enough room for the six-tet cubic stencil and the no-self-loop edge set used by the Dirichlet target.
proof idea
One-line term proof. Convert the flat-configuration hypothesis into a flat-deficit-zero target via FlatDeficitZeroTarget.of_flatConfiguration, then apply the already-proved lemma that zero potential has vanishing Regge action whenever every deficit is zero on the canonical periodic torus.
why it matters
Exact flat normalization is the baseline for every continuum comparison in this gravity track. Downstream, the two-input bundle form reuses it, the damped D2 schedule closure uses it inside the normalized Regge-minus-Dirichlet cubic Taylor bound, and the Track-1B corrected quadratic axis bound feeds the same vanishing into the damped-schedule convergence statement.
In the Recognition gravity program this is the discrete analogue of "flat space has zero Einstein-Hilbert action": without it, the six-tet cubic Dirichlet instance cannot certify that the nonlinear Regge action sits on the correct quadratic Dirichlet limit. It is a proved obligation inside the physical-instance package, not a free axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.