cubic_lattice_deficit_zero
plain-language theorem explainer
The Regge deficit vanishes for the flat cubic lattice when four right dihedral angles sum to 2π. A discrete geometer working on simplicial Regge calculus would cite this to anchor the zero-curvature case before introducing defects. The proof is a direct one-line application of the general deficit-zero lemma to the already-proved flat-sum condition for the cube.
Claim. Let $d$ be the dihedral-angle datum with cosine zero (so each angle equals $π/2$). The deficit function $δ$ on a list of four such data satisfies $δ([d,d,d,d])=0$.
background
The DihedralAngle module represents each dihedral angle by a DihedralAngleData record that stores a cosine value in $[-1,1]$ together with the angle $θ=arccos(cos)$. The deficit at a hinge is the real number $2π$ minus the sum of the four thetas around that edge. The upstream cubic_lattice_flatSum theorem records that four copies of the cube datum satisfy the FlatSumCondition, i.e., their angles add exactly to $2π$ (the classical statement that the integer lattice is flat).
proof idea
One-line wrapper that applies the lemma deficit_eq_zero_of_flat to the list of four cube dihedral data together with the witness cubic_lattice_flatSum.
why it matters
The result populates the cubic_deficit_zero field of the dihedralAngleCert theorem that collects the basic facts required by Schläfli's identity and the Phase C5 simplicial discharge. It supplies the zero-curvature baseline inside the Recognition Science geometry layer, confirming the classical $π/2×4=2π$ identity before defects are introduced. It closes one of the elementary cases needed to linearize the Regge action on general complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.