flat_deficit_zero
plain-language theorem explainer
The flat deficit angle vanishes on the undeformed cubic lattice. Regge calculus and discrete gravity formalizers cite it as the zero-curvature baseline before metric perturbations induce nonzero deficits. The proof is a direct term reduction that unfolds the angle definitions and applies algebraic simplification.
Claim. $δ_{flat} = 0$, where $δ_{flat}$ is the deficit angle at an edge of the flat cubic lattice, given by $2π$ minus the sum of four dihedral angles each equal to $π/2$.
background
The DiscreteCurvature module formalizes Regge-style curvature on lattices by defining deficit angles as $2π$ minus the sum of dihedral angles around each edge. On the flat $Z^3$ lattice every cube has right dihedral angles, so the deficit is identically zero. This supplies the reference case before deformations are introduced via metric perturbations $h$ whose second derivatives source curvature.
proof idea
Term-mode proof: unfold deficit_angle_flat, cubes_per_edge and cube_dihedral, then simp followed by ring reduces the expression to the algebraic identity $2π - 4·(π/2) = 0$.
why it matters
It populates the flat_zero field of discrete_curvature_cert, which certifies the full discrete curvature package including the bridge to second derivatives of $h$ and the Gauss-Bonnet sum. The result anchors the Regge action's convergence to the Einstein-Hilbert integral and confirms zero curvature on the undeformed lattice in the Recognition Science J-cost derivation of gravity in three dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.