ricci_from_source
plain-language theorem explainer
This definition supplies the linearized Ricci scalar R = -κ ρ in Recognition Science gravity, where κ = 8φ⁵. A physicist working on lattice gravity or discrete curvature would cite it when connecting defect density to the Einstein tensor source term. The implementation is a direct multiplication using the upstream kappa_rs definition from ZeroParameterGravity.
Claim. $R = -8φ^5 ρ$ where $ρ$ is the defect density and the factor $8φ^5$ is the RS gravitational coupling.
background
The LatticeRicci module defines the lattice Ricci scalar from deficit angles. From the imported DiscreteCurvature, curvature_from_deficit(d2h, a) = -d2h, and summing over the three spatial axes yields the lattice Ricci scalar as the negative Laplacian of the trace of the metric perturbation. In the linearized weak-field regime with harmonic gauge, this matches the continuum expression R = -∇²(trace h). The upstream result kappa_rs from ZeroParameterGravity provides the RS-specific coupling κ = 8φ⁵, stated as 'The RS prediction for the Einstein gravitational coupling: κ = 8φ⁵. This is derived, not assumed.'
proof idea
This declaration is a one-line wrapper that applies the definition of kappa_rs and scales it by the negative density rho. No additional lemmas or tactics are invoked beyond the direct term substitution from the ZeroParameterGravity import.
why it matters
This definition is used by LatticeRicciCert to establish the attractive property for positive rho and by the proportionality theorem ricci_source_proportional_to_kappa. It completes the linearized Poisson-to-Ricci mapping in the module's Step 4 on lattice Ricci convergence. The parent structure LatticeRicciCert states the full nonlinear Regge convergence as a hypothesis, while this handles the exact linearized match. It ties into the RS forcing chain where the gravitational constant emerges from phi without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.