reggeAction_zeroPotential_eq_zero_of_flatConfiguration
plain-language theorem explainer
On any incidence-consistent 3D triangulation that admits a flat analytic configuration, the concrete Regge action at the zero vertex potential vanishes. Discrete-gravity and Regge-calculus workers cite this as the flat-action normalization before Hessian or Dirichlet comparisons on the six-tet cubic lattice. The proof is a one-line reduction: extract the flat-deficit target from the flat-configuration package, then apply the zero-potential vanishing lemma for flat deficit.
Claim. Let $K$ be an incidence-consistent 3D triangulation. If $K$ carries a flat analytic configuration (arccos endpoint free at the base point, zero deficit angles, and the smoothness package needed for Taylor theory), then the concrete vertex-conformal Regge action of $K$ at the zero vertex potential equals zero: $S_{\mathrm{Regge}}(K,0)=0$.
background
This module packages the exact 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; it assembles the theorem-shaped pieces that make that instantiation possible.
The concrete 3D Regge action under the vertex-conformal ansatz is the edge sum of hinge measure times deficit angle. A flat analytic configuration packages three facts: the arccos endpoint condition at the base point (dihedral cosines squared avoid $\pm 1$), the zero-deficit flatness condition, and the smoothness fact needed to invoke Taylor theory for the full nonlinear action. The zero vertex potential is the base configuration against which the Hessian and Dirichlet comparisons are taken.
Upstream, the flat-configuration structure already encodes zero deficit; a companion target converts that package into the flat-deficit hypothesis used by the zero-potential vanishing lemma for the Regge action.
proof idea
Term-mode one-liner. From the given flat analytic configuration, FlatDeficitZeroTarget.of_flatConfiguration produces the flat-deficit target. That target is fed to reggeAction_zeroPotential_eq_zero_of_flatDeficit, which concludes that the concrete Regge action at the zero vertex potential is zero. No additional algebraic work is done in this declaration.
why it matters
Flat-action normalization is the baseline check before any second-variation or Dirichlet comparison on the six-tet cubic lattice: if the action does not vanish on the flat zero-potential configuration, Hessian and finite-difference Dirichlet targets are meaningless. The module sits in the gravity chain that connects the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model, in spatial dimension $D=3$ as forced by the T8 step of the forcing chain.
No downstream consumers are recorded yet; siblings in the same module (canonical Hessian-is-Dirichlet facts, periodic edge-stencil Dirichlet actions and nonnegativity) are the natural landing sites. The declaration closes the flat-normalization obligation that those Dirichlet and Hessian packages presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.