DiscreteCurvatureCert
plain-language theorem explainer
DiscreteCurvatureCert packages four identities that certify cubic-lattice curvature matches continuum expectations: flat deficit vanishes, deformed deficit divided by a squared recovers minus the second metric derivative, vertex deficit sum equals 4 pi, and the resulting Euler characteristic is 2. Lattice gravity workers cite it when checking that Regge deficits reproduce sectional curvature on Z^3. The structure is assembled directly from four upstream definitions and lemmas already established in the module.
Claim. Let $d^2h$ be the second derivative of the metric perturbation, $a$ the lattice spacing, $K$ the curvature obtained by dividing deficit angle by dual area, and $V$ the total vertex deficit. Then DiscreteCurvatureCert asserts: flat deficit angle equals zero; $K$ of the deformed deficit equals $-d^2h$ for all $a≠0$; $8V=4π$; and $8V/(2π)=2$.
background
The module develops Regge-style discrete curvature on the cubic lattice. Deficit angle at an edge equals 2π minus the sum of dihedral angles around it. On the flat lattice the four right dihedrals sum exactly to 2π, so the deficit is zero. A metric perturbation with second derivative $d^2h$ deforms each dihedral by a term proportional to $a^2 d^2h$, producing deficit angle $-a^2 d^2h$. Curvature is defined as this deficit divided by the dual area $a^2$, recovering exactly $-d^2h$. The vertex deficit for one cube is $2π-3(π/2)=π/2$, hence eight vertices sum to 4π, which is 2π times the Euler characteristic of S^2.
proof idea
The structure is defined by four fields. Each field is supplied by a prior lemma in the same module: flat_zero by flat_deficit_zero, curvature_bridge by curvature_equals_d2h, gauss_bonnet by gauss_bonnet_cube, and euler_char by euler_characteristic_from_deficit. No tactics or additional reasoning are needed; the declaration simply bundles the four already-proved statements.
why it matters
The certificate is instantiated by the theorem discrete_curvature_cert, which supplies concrete values for each field and thereby produces a single object usable in downstream arguments. It supplies the explicit bridge from lattice deficit angles to the continuum Ricci scalar, confirming that the Regge action on the cubic lattice recovers the Einstein-Hilbert term in the continuum limit. The Gauss-Bonnet and Euler-characteristic identities tie the construction to the topology of S^2, consistent with the three-dimensional spatial lattice fixed by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.