pd

The module is a standalone tractability probe for flat FRW ($k=0$, $c=1$) encoded componentwise on Fin 4. Every geometric field depends only on cosmic time $t$, so the continuum partials collapse: $\partial_0 = d/dt$ and $\partial_i \equiv 0$.

Sibling defs supply the diagonal metric $g_{00}=-1$, $g_{ii}=a(t)^2$ and its inverse $g^{00}=-1$, $g^{ii}=1/a(t)^2$. The Christoffel formula of the second kind is written directly in terms of those components and this partial operator: $\Gamma^\lambda_{\mu\nu}=\tfrac12\sum_\sigma g^{\lambda\sigma}(\partial_\mu g_{\nu\sigma}+\partial_\nu g_{\mu\sigma}-\partial_\sigma g_{\mu\nu})$.

The probe targets the classical identities $\Gamma^0_{ii}=a\dot a$ and $\Gamma^i_{0i}=\dot a/a$ before locking a full Einstein-equation skeleton.

Pure definition: case-split on the spacetime index. When $\mu=0$, return Mathlib deriv f; otherwise return the constant-zero function. No lemmas are invoked.

This operator is the differential engine of the FRW componentwise probe. Downstream it appears inside every Christoffel expansion: christoffel_0_00 ($\Gamma^0_{00}=0$), the three spatial probes christoffel_0_11/22/33 ($\Gamma^0_{ii}=a\dot a$), and christoffel_1_01 ($\Gamma^1_{01}=\dot a/a$), as well as the auxiliary deriv_a_sq chain used by those proofs.

Closing those identities is the panel gate before locking Ricci, Einstein tensor, and Friedmann I/II as loop targets. In the broader Recognition chain this sits in the continuum GR layer that must eventually match the discrete ledger and eight-tick structure; the def itself is pure classical differential geometry on a homogeneous background.