pd_sin
plain-language theorem explainer
The partial derivative of a constant-amplitude sine plane wave c sin(k·x) equals (c k_μ) cos(k·x). Anyone computing linearized curvature of real standing waves in the continuum Einstein–Hilbert second variation cites this. The proof is a short chain-rule argument: differentiate the phase in one coordinate, compose with sin, scale by c, and match the partial-derivative definition.
Claim. For any amplitude $c \in \mathbb{R}$, wavevector $k \in (\mathbb{R}^4)$, coordinate direction $\mu \in \{0,1,2,3\}$, and point $x \in \mathbb{R}^4$, the partial derivative satisfies $\partial_\mu\bigl(c\,\sin(k\cdot y)\bigr)\big|_{y=x} = (c\,k_\mu)\,\cos(k\cdot x)$.
background
This module derives the continuum transverse-traceless second variation of $\int R\sqrt{g}$ in 4D from the Levi-Civita connection alone, in the same real-cosine convention used by the discrete Regge midpoint dictionary. Coordinates are points $x:\mathrm{Fin},4\to\mathbb{R}$. The plane-wave phase is the ordinary dot product $k\cdot x$.
The partial $\partial_\mu f(x)$ is defined as the ordinary one-variable derivative of $t\mapsto f(x[\mu\mapsto t])$ at $t=x_\mu$. Upstream, hasDerivAt_phase_update records that this slice of the phase is affine in $t$ with slope $k_\mu$, so it is differentiable with that derivative. The companion identity that updating a coordinate to its own value leaves the point fixed is used to evaluate the chain rule at the base point.
proof idea
Start from differentiability of the phase slice (hasDerivAt_phase_update). Compose with $\sin$ via Mathlib's hasDerivAt_sin and the chain rule; after rewriting the evaluation point with the self-update identity, the derivative of $\sin(\mathrm{phase})$ is $\cos(k\cdot x),k_\mu$. Scale by the constant $c$, unfold the partial-derivative definition, and finish with ring to rearrange $(c\cdot(\cos\cdot k_\mu))$ into $(c,k_\mu)\cos$.
why it matters
Linearized Christoffel symbols of a cosine metric perturbation involve derivatives of both cosine and sine amplitudes. This lemma supplies the sine half; its cosine twin handles the other. Downstream, linRicci_eq applies both when differentiating linearized Christoffels to obtain the linearized Ricci tensor as an amplitude times $\cos(k\cdot x)$.
That identity is a step toward the continuum second-variation number for a real TT plane wave, which this arc derives independently of the Regge coupling table so the discrete-to-continuum normalization comparison is non-circular. It sits in Arc 2, step 7 of the gravity analysis, not in the T0–T8 forcing chain, but it is the analytic engine behind matching continuum EH to the banked Regge Hessian convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.