deficit_zero_when_flat
plain-language theorem explainer
The declaration shows that the deficit angle on a deformed cubic lattice vanishes identically when the second derivative of the metric perturbation is zero. Lattice gravity researchers would cite it to confirm the flat-space limit of Regge calculus before introducing curvature. The proof is a one-line algebraic reduction that unfolds the deformed-deficit definition and normalizes the resulting expression.
Claim. For any real lattice spacing $a$, the deficit angle at an edge of the deformed lattice satisfies $d(a) = 0$ whenever the second derivative of the metric perturbation vanishes.
background
The module formalizes discrete curvature on a cubic lattice via deficit angles in the style of Regge calculus. The deficit at a hinge is $2π$ minus the sum of the dihedral angles around the edge; on an undeformed lattice these angles are all $π/2$ so the deficit is identically zero. When a metric perturbation $h$ deforms the lattice, each dihedral angle changes by an amount proportional to the second derivative of $h$, and the net deficit angle is defined to be $-a^2$ times that second derivative.
proof idea
The proof is a one-line wrapper that unfolds the definition of deficit_angle_deformed and applies the ring tactic to verify the algebraic identity.
why it matters
This result anchors the zero-curvature limit inside the discrete-curvature module, confirming that constant or linear $h$ produces no edge curvature. It supports the subsequent claims that deficit angles scale with the square of the lattice spacing and that their sum yields the linearized Ricci tensor. In the Recognition framework it realizes the flat-space case of the Regge action before the J-cost strain is introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.