pd
plain-language theorem explainer
Coordinate partial on flat FRW: the time slot is ordinary d/dt, and every spatial slot is identically zero by homogeneity. Cosmology and GR formalizers cite it whenever Christoffel or Ricci components are expanded as finite Fin-4 sums. The body is a one-line case split on the index.
Claim. For $\mu\in\{0,1,2,3\}$ and $f:\mathbb{R}\to\mathbb{R}$, the coordinate partial is $\partial_\mu f := f'$ if $\mu=0$, and $\partial_\mu f := 0$ otherwise (spatial derivatives vanish by homogeneity).
background
Module target is Layer-1 FRW geometry in a componentwise Fin 4 encoding: flat metric with signature $(-,+,+,+)$, $c=1$, $k=0$. Metric components are diagonal, $g_{00}=-1$ and $g_{ii}=a(t)^2$; the inverse is $g^{00}=-1$ and $g^{ii}=1/a(t)^2$. All curvature objects are finite sums of time derivatives, so no analytic convergence issues arise.
Homogeneity of the FRW background forces every spatial coordinate derivative of metric components to vanish. The only surviving derivative is the ordinary real derivative along cosmic time. That is exactly what this partial encodes: index $0$ routes to deriv, indices $1,2,3$ return the zero function.
Upstream metric and inverse metric definitions supply the $g_{\mu\nu}$ and $g^{\lambda\sigma}$ that the Christoffel formula differentiates through this partial.
proof idea
Pure definition by cases: if the spacetime index equals the time slot $0$, return the Mathlib derivative of $f$; otherwise return the zero function. No lemmas are applied. Downstream simp scripts unfold the case split together with the diagonal metric and inverse metric.
why it matters
Every Christoffel component in the module is written as $\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})$, and each $\partial$ is this partial. Parent results include $\Gamma^0_{00}=0$, $\Gamma^0_{ii}=a\dot a$, and the mixed $\Gamma^i_{0i}$ shapes that feed Ricci, the Einstein tensor, and finally Friedmann I/II as theorems from named Einstein equations plus a comoving perfect fluid.
In the Recognition cosmo chain this is scaffolding for Target C: upgrade bare Friedmann props to derived GR consequences on FRW. It does not touch the forcing chain (T5–T8) or RCL; it is classical differential geometry under RS units $c=1$. The probe file already closed the two key Christoffel shapes; this definition is the shared derivative primitive those proofs and the skeleton sorries both unfold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.