gauss_bonnet_cube
plain-language theorem explainer
The theorem shows that the summed deficit angles over the eight vertices of a cubic lattice total exactly 4π. Lattice gravity researchers cite it to confirm that the discrete curvature measure respects the topology of the 2-sphere. The proof is a one-line algebraic reduction that substitutes the explicit vertex deficit definition and simplifies.
Claim. In cubic lattice geometry the total angular deficit satisfies $8δ_v=4π$, where $δ_v$ is the deficit angle at each vertex obtained from the deviation of summed dihedral angles from $2π$.
background
The DiscreteCurvature module encodes curvature on a deformed cubic lattice via deficit angles in the style of Regge calculus. The deficit at a vertex equals $2π$ minus the sum of the dihedral angles meeting there; these angles are zero in the flat case and nonzero under metric strain. The J-cost of neighboring ledger entries supplies the quadratic strain that produces the deficits. The module builds on upstream dihedral-angle definitions and ledger-factorization structures that calibrate the strain measure.
proof idea
The proof is a one-line wrapper. It rewrites the vertex deficit using its explicit algebraic value and applies ring normalization to reach the constant $4π$.
why it matters
The result is invoked inside the discrete curvature certificate and the Euler-characteristic derivation. It verifies that the integrated deficit equals $4π$, reproducing the Euler characteristic of 2 for the sphere and thereby confirming global topological consistency. Within the Recognition framework this anchors the discrete geometry to the forced three-dimensional structure and supports the Regge action converging to the Einstein-Hilbert action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.