continuum_ricci_linearized
plain-language theorem explainer
The definition supplies the continuum expression for the linearized Ricci scalar as the negative sum of three second derivatives of the metric trace perturbation. Researchers comparing lattice Regge calculus to weak-field general relativity cite this when establishing exact matching in the harmonic gauge. It is realized as a direct algebraic identification of the trace Laplacian without additional lemmas.
Claim. In linearized gravity with metric $g = η + h$ in harmonic gauge, the Ricci scalar is $R = -∇²(trace h)$, represented here as $R = -(d²h_{xx} + d²h_{yy} + d²h_{zz})$ where the three arguments are the indicated second partial derivatives of the trace perturbation.
background
The module defines lattice Ricci from deficit angles and proves convergence to the continuum expression in the linearized weak-field regime. Deficit at a hinge is $2π - Σ θ$ from the DihedralAngle and Schlaefli upstream definitions, which feed curvature_from_deficit(d2h, a) = -d2h. In the local setting, lattice Ricci sums these over three axes while the continuum side uses the standard harmonic-gauge formula R = -∇²(trace h) from linearized GR.
proof idea
This is a one-line definition that directly encodes the harmonic-gauge formula by summing the three diagonal second-derivative components of the trace perturbation.
why it matters
This definition anchors the linearized convergence theorem lattice_ricci_equals_continuum, which states exact equality between lattice and continuum Ricci scalars. It fills the linearized case in the module's Step 4 on lattice Ricci scalar convergence, while the full nonlinear Regge convergence remains a hypothesis in LatticeRicciCert. It connects to the Recognition framework's treatment of curvature via deficit angles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.