palatini_identity
plain-language theorem explainer
The Palatini identity equates the variation of the Ricci tensor to covariant derivatives acting on the variation of the connection coefficients. Derivations of the Einstein equations from the Hilbert action cite this step as the bridge between the curvature variation and the connection change. The declaration is a structural definition that asserts the identity holds as a proposition without executing the explicit nabla computation.
Claim. The Palatini identity asserts that for any variation $delta_gamma$ of the connection coefficients, the corresponding variation of the Ricci tensor satisfies $delta R_{mu nu} = nabla_rho (delta Gamma^rho_{mu nu}) - nabla_nu (delta Gamma^rho_{mu rho})$.
background
The Einstein-Hilbert action module defines the action as $S_{EH}[g] = (1/2 kappa) integral R sqrt(-g) d^4x$ and shows that its metric variation produces the Einstein tensor, thereby proving Axiom 2. The Palatini identity supplies the curvature-variation piece required for that calculation. Upstream results supply the Kronecker delta on Fin n for index contractions and the flat affine connection used to define nabla; the RicciTensor module provides the contraction that turns the Riemann tensor into R_mu nu.
proof idea
One-line wrapper that directly returns the universal quantification over delta_gamma of True, with an inline comment noting that the full nabla expression awaits the complete connection implementation.
why it matters
This supplies the missing structural link inside the Hilbert variation proof that converts the action variation into the Einstein tensor and hence the vacuum field equations G_mu nu = 0. It sits inside the chain that derives classical gravity from the Recognition Science forcing structure (T0-T8) once the phi-ladder constants and J-cost are fixed. No downstream uses are recorded yet, leaving the explicit connection computation as the remaining closure step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.