cubic_flat_deficit
plain-language theorem explainer
On the cubic lattice ℤ³, each edge meets four right dihedral angles, so the Regge deficit is exactly zero. Gravity and Regge-calculus workers cite this as the flat-background identity for the RS cubic case. The proof is a one-line term wrapper of the ring-closed lattice-flatness lemma.
Claim. The angular deficit around an edge of the flat cubic lattice vanishes: $2\pi - 4\cdot(\pi/2) = 0$. Each of the four cubes sharing the edge contributes dihedral angle $\pi/2$, summing to a full $2\pi$.
background
In Regge calculus, curvature is concentrated on hinges (edges in 3D). The deficit angle at an edge is $2\pi$ minus the sum of dihedral angles of the cells meeting there. Vanishing deficit means locally flat geometry.
This module replaces the general Cheeger–Müller–Schrader convergence axiom by a direct argument specialized to Recognition Science: J-cost interactions on the cubic lattice ℤ^D, with known Taylor structure $J(e^\varepsilon)=\cosh\varepsilon-1$. The cubic case is rigid: every cell is identical and every interior dihedral angle is $\pi/2$.
Upstream, cubic_lattice_flat already records the same arithmetic identity ("each edge is shared by 4 cubes... Sum = 4·π/2 = 2π, so deficit = 0"). The present declaration re-exports that fact inside the CubicReggeProof development.
proof idea
One-line term wrapper: the goal is definitionally the statement of ReggeCalculus.cubic_lattice_flat, which itself closes by ring on the real arithmetic $2\pi-4(\pi/2)=0$. No extra geometric hypotheses are discharged here.
why it matters
Flat deficit is the vacuum baseline for the cubic Regge chain. Downstream, proved_convergence_chain and cubic_regge_convergence_cert assemble the full RS lattice-to-linearized-EFE derivation with zero axioms and zero sorry; both list a flat-solution step that rests on this identity (constants satisfy the discrete EL equation precisely because the background deficit is zero).
In the module strategy this is Tier-0 geometry supporting Tier 2 (EL linearizes to the lattice Laplacian via $\sinh'(0)=1$) and Tier 3 (Laplacian$/a^2\to\nabla^2$). It is the discrete counterpart of Minkowski space before continuum recovery of the linearized Einstein equation. Framework-wise it sits in the gravity sector that takes the forced $D=3$ (T8) cubic lattice as the RS spatial skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.