vertex_deficit_value
plain-language theorem explainer
The theorem fixes the angular deficit per vertex of a cubic cell at exactly π/2. Regge-calculus and discrete-gravity workers cite the value when summing deficits to recover the Euler characteristic on Z^3. The proof is a one-line wrapper that unfolds the deficit definition together with the cube dihedral angle and reduces the arithmetic by ring.
Claim. Let $δ_v := 2π - 3·(π/2)$ be the angular deficit at each vertex of the unit cube, where the dihedral angle between adjacent faces is π/2. Then $δ_v = π/2$.
background
The DiscreteCurvature module treats curvature on the cubic lattice via deficit angles in the style of Regge calculus. At each vertex three faces meet; the deficit is therefore 2π minus three times the dihedral angle. The sibling definition vertex_deficit_cube encodes exactly this expression, while cube_dihedral supplies the constant value π/2 for the right angle of the cube. The module document states that on a flat Z^3 lattice the total deficit summed over eight vertices equals 4π, recovering 2π·χ(S²) with χ=2.
proof idea
The proof is a one-line wrapper. It unfolds vertex_deficit_cube and cube_dihedral, exposing the arithmetic 2π - 3·(π/2), then invokes ring to obtain π/2.
why it matters
The result supplies the numerical value required by the immediate downstream theorem gauss_bonnet_cube, which states 8·vertex_deficit_cube = 4π and thereby confirms the Gauss-Bonnet identity for the cube. Within the Recognition framework the identity anchors the discrete curvature step that later connects J-cost strain to sectional curvature in the quadratic limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.