deficit_zero_when_flat
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute the deficit angle for nonzero second derivatives of $h$.
- Does not derive the proportionality factor $a^2$ from the underlying J-cost.
- Does not address non-cubic lattices or higher-order curvature terms.
- Does not treat global topology or the Gauss-Bonnet theorem.
formal statement (Lean)
79theorem deficit_zero_when_flat (a : ℝ) : deficit_angle_deformed 0 a = 0 := by
proof body
Term-mode proof.
80 unfold deficit_angle_deformed; ring
81
82/-- The deficit angle scales with the lattice spacing squared. -/