ricci_is_sum_of_curvatures
plain-language theorem explainer
The theorem equates the linearized Ricci tensor assembled from the three second derivatives of the metric perturbation to the sum of three curvature terms, each obtained from a deformed deficit angle scaled by lattice spacing squared. Discrete gravity and Regge-calculus workers cite it to confirm additive curvature emergence on a deformed cubic lattice. The proof is a one-line wrapper that rewrites each curvature term via its equality to the second derivative and finishes with ring arithmetic.
Claim. Let $d_{2h_x}, d_{2h_y}, d_{2h_z}, a$ be real numbers with $a ≠ 0$. Then the linearized Ricci curvature constructed from the three second derivatives equals the sum of the three curvatures obtained from the deformed deficit angles: linearized Ricci from deficits$(d_{2h_x}, d_{2h_y}, d_{2h_z}) = ∑_{i=x,y,z}$ curvature from deficit(deficit angle deformed$(d_{2h_i}, a), a^2)$.
background
The Discrete Curvature module formalizes Regge-style curvature on a cubic lattice. The deficit angle at an edge is $δ_e = 2π −$ sum of dihedral angles around the edge; it is zero on the flat $Z^3$ lattice and nonzero once a metric perturbation $h$ deforms the dihedral angles. In the Recognition Science setting the J-cost of neighboring ledger entries supplies the strain whose second derivative yields the deficit angle (approximately $½(log ratio)^2$). The module proves that deficit angles are proportional to second derivatives of $h$, vanish when $h=0$, and sum to $4π$ over the eight vertices of a cube, recovering the Gauss-Bonnet theorem for $S^2$.
proof idea
The proof is a one-line wrapper. It applies simp with the lemma curvature_equals_d2h (valid under $a ≠ 0$) to replace each curvature_from_deficit term by the corresponding second derivative, then invokes the definition of linearized_ricci_from_deficits on the left-hand side and closes with the ring tactic.
why it matters
The identity shows that linearized Ricci curvature on the discrete lattice is exactly the sum of the three directional curvature contributions from deformed deficit angles. It therefore supplies the local curvature measure required for the Regge action inside the Recognition Science framework, where J-cost strain deforms the lattice. The result bridges the basic deficit-angle lemmas and the Gauss-Bonnet statement that follows it in the module; it works explicitly with the three coordinate directions fixed by the T8 step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.