flat_deficit_zero
plain-language theorem explainer
In Regge calculus on the RS lattice, hinge data whose dihedral angles sum exactly to 2π has vanishing deficit angle. Discrete curvature certificates and flat-lattice constructions cite this zero-curvature case. The proof is a one-line unfolding of the deficit definition followed by linear arithmetic on the sum hypothesis.
Claim. For hinge data $h$ with dihedral angles satisfying $h.dihedral_angles.sum = 2π$, the deficit angle satisfies $δ(h) = 0$, where $δ(h) = 2π - ∑ θ_i$.
background
The Regge calculus module discretizes spacetime into a simplicial complex on the Z^3 × Z lattice with edge lengths from the J-cost defect field. HingeData is a structure holding an area (positive real) and a list of dihedral angles contributed by all simplices meeting at a codimension-2 hinge; the deficit is defined as 2π minus the sum of those angles. The module replaces linearized deficit-angle assumptions with the exact nonlinear Regge action S = ∑ A_h δ_h.
proof idea
The proof is a one-line wrapper that unfolds the sibling definition of deficit_angle and applies linear arithmetic to the hypothesis that the sum of dihedral angles equals 2π, immediately yielding zero.
why it matters
This theorem supplies the flat_zero component of the discrete curvature certificate, which also assembles the curvature bridge and Gauss-Bonnet relation. It confirms that the Regge action vanishes on flat configurations, consistent with the forcing chain's D = 3 and eight-tick octave. The result closes the zero-curvature case before deformed-lattice extensions are considered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.