deficit_eq_zero_of_flat
plain-language theorem explainer
The theorem states that a list of dihedral angle data satisfying the flat sum condition (sum of angles equals 2π) yields zero deficit. Workers on Regge calculus or simplicial gravity discretizations cite it as the baseline identity for flat hinges. The proof is a direct algebraic reduction: unfold the deficit definition, rewrite with the sum hypothesis, and simplify via ring.
Claim. Let $ds$ be a list of dihedral angle data. If the sum of the angles satisfies $sumThetas(ds) = 2π$, where each angle is $arccos$ of the cosine value in the datum, then the deficit $2π - sumThetas(ds)$ equals zero.
background
DihedralAngleData is a structure holding a cosine value in $[-1,1]$, from which the angle theta is recovered as $arccos(cosine)$ and lies in $[0,π]$. FlatSumCondition on a list $ds$ asserts that the sum of these thetas equals $2π$. The deficit function is defined as $2π$ minus that sum of thetas, matching the standard Regge expression for angular defect at a hinge.
proof idea
The proof unfolds the definition of deficit to obtain $2π - sumThetas ds$, rewrites the sum using the FlatSumCondition hypothesis, and applies the ring tactic to conclude the difference is identically zero. It is a one-line algebraic wrapper once the sum condition is supplied.
why it matters
This identity supplies the flat-hinge base case in the dihedral angle module (Phase C2). It is invoked directly by cubic_lattice_deficit_zero to recover the zero-deficit result for four cube dihedrals and by totalDeficit_flat in the Schlaefli module to show that universal flat-sum conditions imply vanishing total deficit. The result closes the flat contribution needed before threading the setup into the full simplicial discharge of the Regge linearization hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.