curvature_equals_d2h
plain-language theorem explainer
The equality shows that curvature computed from a deformed-lattice deficit angle recovers exactly the negative second derivative of the metric perturbation. Researchers modeling discrete gravity or Regge calculus would cite this as the direct lattice-to-continuum bridge. The proof is a short algebraic reduction obtained by unfolding the two defining expressions and simplifying with field operations and the ring tactic.
Claim. Let $K$ be the curvature obtained from a deficit angle and hinge area, and let $d_2h$ be the second derivative of a metric perturbation on a lattice of scale $a$. Then $K$ applied to the deformed deficit angle at scale $a$ equals $-d_2h$ whenever $a$ is nonzero.
background
The DiscreteCurvature module formalizes Regge-style curvature on a cubic lattice. The deficit angle at an edge is $2pi$ minus the sum of dihedral angles around that edge; it vanishes on the flat lattice and becomes nonzero under a metric perturbation $h$. The module shows that these deficits are proportional to second derivatives of $h$, that they vanish when $h=0$, and that their area-normalized sum converges to sectional curvature.
proof idea
The proof unfolds the definitions of curvature_from_deficit and deficit_angle_deformed, records that $a^2$ is nonzero, then applies field_simp followed by ring to obtain the identity.
why it matters
This supplies the curvature bridge used by discrete_curvature_cert and invoked inside ricci_is_sum_of_curvatures and lattice_ricci_equals_continuum. The latter states that the lattice Ricci scalar equals the continuum linearized Ricci scalar exactly. The result closes the discrete-to-continuum step for gravity in the Recognition framework, consistent with Regge's convergence of the Regge action to the Einstein-Hilbert action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.