reggeAction_zeroPotential_eq_zero_of_flatDeficit
plain-language theorem explainer
If every edge deficit vanishes on the zero vertex potential, the concrete 3D Regge action is identically zero. Discrete-gravity and Regge-calculus workers cite this as the finite-sum step that normalizes the flat background before quadratic expansion. The proof unfolds the edge-sum definition and kills each summand by deficit-zero times the hinge measure.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Write $\xi_0$ for the identically zero vertex potential. If the deficit angle of $\xi_0$ vanishes at every edge of $K$, then the Regge action of $K$ at $\xi_0$ equals $0$.
background
The ambient module packages exact theorem obligations that 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 reduces that claim to geometric targets on the triangulation.
The concrete 3D Regge action under the vertex-conformal ansatz is the edge sum $\sum_e m_e(\xi),\delta_e(\xi)$, where $m_e$ is the hinge measure and $\delta_e$ is the deficit angle at edge $e$. The deficit itself is the classical hinge quantity $2\pi-\sum\theta$ of incident dihedral angles. The zero potential $\xi_0$ is the flat background configuration on the vertices.
The hypothesis "flat-deficit zero target" is the exact geometric input for flat-action normalization: for every edge $e$, $\delta_e(\xi_0)=0$. An equivalent angle-sum form asks that the incident local dihedral contributions around each global edge sum to $2\pi$. The remaining periodic-Freudenthal task is to discharge this target from the canonical flat geometry.
proof idea
Term-mode, four steps. Unfold the Regge action to its defining finite sum over edges of hinge-measure times deficit angle. Apply the standard Finset fact that a sum is zero once every summand is zero. On a generic edge, rewrite the deficit factor by the flat-deficit hypothesis (pointwise zero at the zero potential), then finish with multiplication by zero. No geometric estimate is needed beyond the hypothesis.
why it matters
This is the finite-sum reduction behind the flat-action zero input used by the scaled quadratic normalization layer in the six-tet cubic Dirichlet pipeline. Downstream, the canonical periodic specialization applies it on the encoded periodic Freudenthal torus once flat deficit zero is known there, and the flat-configuration package routes through it by first converting a full flat-configuration hypothesis into the deficit-zero target.
In the broader gravity stack the lemma sits under the physical six-tet cubic Dirichlet instance that bridges the periodic Freudenthal scaffold to the Dirichlet model target. Flat-background normalization is a prerequisite for reading off a discrete Dirichlet (or Hessian) quadratic form from the Regge action; without action zero on the flat potential, the constant term pollutes the quadratic layer. It is pure 3D Regge bookkeeping, not a forcing-chain (T0–T8) step, but it is load-bearing for the discrete gravity side of the Recognition lattice program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.