vertex_deficit_cube
plain-language theorem explainer
The angular deficit at each vertex of a cube is defined as twice pi minus three times the cube dihedral angle. Lattice gravity and Regge calculus researchers cite this when verifying total curvature on cubic discretizations of S^2. The definition is a direct algebraic expression that substitutes the fixed right dihedral angle.
Claim. The angular deficit at each vertex of a cube is given by $2π - 3·(π/2)$.
background
The DiscreteCurvature module formalizes Regge-style curvature on a cubic lattice. Deficit angles measure deviation from flat space: at each vertex three square faces meet, and the local deficit is 2π minus the sum of the three dihedral angles. The module shows that these deficits sum to 4π on the sphere, recovering the Euler characteristic via Gauss-Bonnet.
proof idea
One-line definition that subtracts three times the upstream cube_dihedral value from 2π. It directly uses the constant π/2 supplied by cube_dihedral in Constants.AlphaDerivation and Geometry.DihedralAngle.
why it matters
This supplies the per-vertex deficit that gauss_bonnet_cube and euler_characteristic_from_deficit combine to recover 4π and χ(S²)=2. It anchors the discrete Gauss-Bonnet step inside the Recognition Science treatment of curvature as J-cost strain on the lattice, feeding the DiscreteCurvatureCert structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.