cubic_lattice_flat
plain-language theorem explainer
The declaration shows that four dihedral angles of π/2 each sum to exactly 2π on the cubic lattice Z³, yielding zero deficit angle and confirming flat geometry. Discrete gravity researchers using Regge calculus would reference this as the vanishing-curvature baseline for the RS lattice. The proof reduces to a trivial ring computation verifying the arithmetic identity 2π - 2π = 0.
Claim. On the flat cubic lattice, the sum of dihedral angles around each edge is $4 times pi/2 = 2pi$, so the deficit angle vanishes.
background
Regge calculus models gravity on a simplicial complex where curvature concentrates at codimension-2 hinges. The deficit angle equals 2π minus the sum of dihedral angles contributed by adjacent simplices. In the Recognition Science setting the spatial lattice is Z³ with edge lengths fixed by the J-cost defect field, and each edge is shared by four cubes.
proof idea
The proof is a one-line wrapper that applies the ring tactic to simplify the arithmetic expression directly to zero.
why it matters
This supplies the flat baseline inside the Regge calculus certification theorem, which assembles flat_vanishes, cubic_flat, and the sign conditions on deficits. It recovers the classical statement that the Z³ lattice is flat, as used by the downstream flat-sum theorem. The result anchors the zero-curvature sector of the framework before J-cost defects are introduced to generate nonzero curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.