eh_proportional_to_R
plain-language theorem explainer
The Einstein-Hilbert Lagrangian density scales directly with the scalar curvature R, so the ratio of densities for two curvatures equals R1 over R2 when kappa is positive and the metric determinant is nonzero. Researchers deriving the Einstein equations via the variational principle cite this to confirm the action density is linear in R after fixing the coupling and volume factor. The proof unfolds the density definition by simplification, introduces positivity facts for the square root and twice kappa, then cancels common terms by field_simp.
Claim. Let $L(R, g, kappa)$ denote the Einstein-Hilbert Lagrangian density. For real numbers $R_1, R_2, det_g, kappa$ with $kappa > 0$ and $|det_g| > 0$, $L(R_1, det_g, kappa) / L(R_2, det_g, kappa) = R_1 / R_2$.
background
The module defines the Einstein-Hilbert action as the integral of R times the square root of the absolute metric determinant, scaled by 1 over 2 kappa, and proves its variation yields the Einstein tensor. The Lagrangian density is therefore the integrand factor proportional to the scalar curvature R. This theorem isolates the proportionality by showing that all dependence on the determinant and coupling cancels in the ratio of two densities. The local setting is the proof of Axiom 2 (Hilbert variation) from the preceding definitions of the Riemann and Ricci tensors.
proof idea
The tactic proof applies simp to unfold the Lagrangian density definition. It then constructs positivity witnesses for the square root of the absolute determinant and for twice kappa. Field_simp is invoked with the non-zero facts to cancel the shared positive factors, leaving the ratio of the two curvature values.
why it matters
This result supplies the proportionality needed for the Hilbert variation theorem in the same module, which derives the vacuum Einstein equations from stationarity of the action. It anchors the gravity sector of Recognition Science by confirming the standard Einstein-Hilbert form before the forcing chain imposes D equals 3 and the phi-ladder structure on masses. The declaration closes the definition step for the action density with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.