pd
plain-language theorem explainer
Coordinate partial derivative of a scalar field on 4D Euclidean space: fix all but the μ-th slot and differentiate in that real parameter. Gravity analysts cite it as the sole differential operator feeding the linearized Christoffel and Ricci constructions in the continuum TT second-variation derivation. The body is a one-line Mathlib `deriv` of the coordinate-update section.
Claim. For a coordinate index $\mu \in \{0,1,2,3\}$, a scalar field $f:\mathbb{R}^4\to\mathbb{R}$, and a point $x\in\mathbb{R}^4$, the partial derivative in direction $\mu$ is $\partial_\mu f(x) := \frac{d}{dt}\big|_{t=x_\mu} f(x[\mu\mapsto t])$, where $x[\mu\mapsto t]$ replaces the $\mu$-th coordinate of $x$ by $t$.
background
The ambient module derives the continuum transverse-traceless second variation of the Einstein-Hilbert integrand $\int R\sqrt{g}$ in 4D, matching the real-cosine plane-wave convention used by the banked Regge midpoint dictionary. Non-circularity is structural: only Mathlib and a pure linear-algebra edge-TT module are imported, so no discrete coefficient can leak in.
Points are maps $x:\mathrm{Fin},4\to\mathbb{R}$. The plane-wave phase is the ordinary dot product $k\cdot x$. All subsequent linearized curvature objects (Christoffel, Ricci) are built by applying this partial to components of a real standing wave $h_{\mu\nu}(x)=H_{\mu\nu}\cos(k\cdot x)$.
Named classical input A1 in the module doc is the linearized Levi-Civita symbol $\Gamma^{(1)}{\lambda\mu\nu}=\tfrac12(\partial\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu})$, which is written directly in terms of these partials.
proof idea
Definitional one-liner. The scalar is restricted to the affine line that varies only the $\mu$-th coordinate via Function.update, then Mathlib deriv is evaluated at the original coordinate value $x_\mu$. No lemmas are invoked at the definition site; differentiability obligations appear later in pd_cos and pd_sin via hasDerivAt_phase_update and the chain rule for Real.cos/Real.sin.
why it matters
This is the unique differential primitive of Arc 2 step 7. Downstream, linChristoffel (A1) and linRicci (A2) are pure combinations of pd applied to the plane-wave metric perturbation; linRicci_eq then closes the cosine amplitude. The proved identities pd_cos and pd_sin carry the real-standing-wave convention into the second-variation number that is later compared, in a separate module, against the Regge dictionary factor.
The module exists because the discrete bookkeeping factor 2 was previously an underived definition bridging continuum $-1/8$ and preflight $-1/4$; deriving the continuum side independently from Levi-Civita alone is the honest check. The same partial also appears in FRW cosmology probes (scale-factor derivatives, Christoffel components), so the notation is shared beyond pure TT gravity analysis.
No Recognition forcing-chain landmark (T5–T8, RCL, $\phi$) is at stake here; the declaration is classical differential geometry scaffolding inside the gravity continuum bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.