discrete_curvature_cert
plain-language theorem explainer
The discrete curvature certificate asserts that deficit angles on a cubic lattice vanish in the flat case, bridge to continuum curvature via second derivatives of the metric, satisfy Gauss-Bonnet, and yield Euler characteristic 2. Lattice gravity researchers would cite it to validate the Regge-style discretization. The proof is a term-mode construction that directly supplies four upstream lemmas as the structure fields.
Claim. There exists a certificate $C$ such that the flat deficit angle vanishes ($δ_{flat}=0$), the curvature from a deformed deficit equals the negative second derivative of the metric perturbation ($κ(δ(d_2h,a),a^2)=-d_2h$ for $a≠0$), the Gauss-Bonnet relation holds ($8×δ_{vertex}=4π$), and the Euler characteristic is recovered ($8×δ_{vertex}/(2π)=2$).
background
The module formalizes discrete curvature on a cubic lattice via deficit angles in the style of Regge calculus. On flat Z^3 each cube has dihedral angles π/2; a metric perturbation h deforms these angles so that the deficit at an edge is δ_e=2π minus the sum of dihedral angles around the edge. In the flat case δ_e=0; in the deformed case the deficit is proportional to the second derivative d²h of the perturbation. The structure DiscreteCurvatureCert packages four properties: flat_zero, the curvature bridge, the Gauss-Bonnet sum, and the Euler characteristic of S² equal to 2. The upstream theorem curvature_equals_d2h supplies the key bridge: curvature_from_deficit(deficit_angle_deformed d2h a, a²) = -d2h.
proof idea
The proof is a term-mode construction of the DiscreteCurvatureCert structure. It supplies the flat_zero field with the flat_deficit_zero lemma, the curvature_bridge field with curvature_equals_d2h, the gauss_bonnet field with gauss_bonnet_cube, and the euler_char field with euler_characteristic_from_deficit.
why it matters
This declaration certifies the internal consistency of the deficit-angle formulation inside the gravity module. It supplies the discrete-to-continuum link required for the quadratic J-cost strain picture and the Regge action convergence claim. The result sits at the end of the discrete curvature development and relates to the D=3 spatial dimensions and eight-tick octave in the forcing chain, though no downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.