linearized_ricci_from_deficits
plain-language theorem explainer
This definition encodes the linearized Ricci scalar as the negative sum of second derivatives of the metric perturbation along the three coordinate axes. It is cited in lattice gravity calculations that match Regge deficit angles to the continuum limit of the Einstein-Hilbert action. The implementation is a direct algebraic sum with an overall minus sign.
Claim. $R = - (d^2 h / dx^2 + d^2 h / dy^2 + d^2 h / dz^2)$ for the trace-reversed scalar perturbation in harmonic gauge, where each term is the second derivative of the metric perturbation along one spatial axis.
background
The module develops discrete curvature on a cubic lattice via deficit angles in the style of Regge calculus. On the flat lattice each cube has dihedral angles of pi/2, so the deficit angle at an edge is zero. Metric perturbations deform the dihedral angles; the resulting deficit at each edge is proportional to the second derivative of the perturbation. The J-cost of neighboring ledger entries supplies the strain whose quadratic approximation yields these second derivatives up to lattice-area normalization.
proof idea
The definition is a direct algebraic expression that negates the sum of the three supplied second-derivative terms.
why it matters
It is invoked by the theorem ricci_is_sum_of_curvatures to equate the continuum Ricci scalar to the sum of curvatures obtained from deformed deficit angles. This supplies the explicit link between the J-cost strain on the lattice and the linearized Einstein-Hilbert action, supporting the convergence of the Regge action to its continuum counterpart in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.