euler_characteristic_from_deficit
plain-language theorem explainer
The total angular deficit summed over the eight vertices of a cubic lattice equals 4π, so dividing by 2π recovers the Euler characteristic 2 of the 2-sphere. This identity confirms the discrete Gauss-Bonnet theorem for the cube in a Regge-style lattice. Lattice gravity researchers would cite it to certify that integrated curvature matches topology. The proof is a direct algebraic reduction from the prior Gauss-Bonnet identity for the cube.
Claim. Let $V$ be the total deficit angle summed over the eight vertices of the cube. Then $8V/(2π)=2$.
background
The module formalizes discrete curvature on a cubic lattice via deficit angles in the style of Regge calculus. The deficit angle at an edge is δ_e = 2π minus the sum of dihedral angles around that edge; on a flat lattice all deficits vanish. The vertex_deficit_cube definition aggregates these deficits over the eight vertices of the cube, each contributing π/2 when dihedral angles are π/2. The upstream gauss_bonnet_cube theorem states that the sum of all deficits equals 4π, which is exactly 2π times the Euler characteristic of S².
proof idea
One-line wrapper that applies the gauss_bonnet_cube theorem to replace the left-hand side, then invokes field_simp on the nonzero π factor followed by ring to obtain the arithmetic identity 2=2.
why it matters
This theorem supplies the Euler-characteristic component inside the discrete_curvature_cert certificate. It closes the Gauss-Bonnet step of the discrete curvature module, confirming that the total deficit reproduces χ(S²)=2. In the Recognition Science setting it anchors the emergence of spatial curvature from J-cost strain on the lattice, consistent with the eight-tick octave and D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.