pd_cos
plain-language theorem explainer
The partial derivative of a real cosine plane wave c cos(k·x) in direction μ equals −c k_μ sin(k·x). Anyone computing the linearized Christoffel symbols for a real standing-wave metric perturbation cites this. The proof chains the chain rule through the phase derivative, multiplies by the constant amplitude, and simplifies.
Claim. For any amplitude $c \in \mathbb{R}$, wavevector $k : \mathbb{R}^4$, coordinate direction $\mu \in \{0,1,2,3\}$, and point $x \in \mathbb{R}^4$, $$\partial_\mu\bigl(c\,\cos(k\cdot x)\bigr) = -c\,k_\mu\,\sin(k\cdot x).$$
background
This module (Arc 2, step 7) derives the continuum transverse-traceless second variation of $\int R\sqrt{g}$ in 4D from the Levi-Civita connection alone, under the same real-cosine convention used by the banked 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 derivative operator $\partial_\mu$ is defined as the ordinary one-variable derivative of $t \mapsto f(x[\mu\mapsto t])$ evaluated at $t = x_\mu$. Upstream, hasDerivAt_phase_update records that $t \mapsto k\cdot x[\mu\mapsto t]$ has derivative $k_\mu$ at $x_\mu$, which is the only analytic input needed here.
The real standing-wave convention (not a complex exponential) is forced by matching the discrete Bloch symbol, whose coupling weight already encodes the lattice average of $\cos(k\cdot m)\cos(k\cdot m')$.
proof idea
Start from hasDerivAt_phase_update: the phase along the $\mu$-line has derivative $k_\mu$. Compose with Mathlib's HasDerivAt for cosine to get
$$\frac{d}{dt}\cos\bigl(\mathrm{phase},k,x[\mu\mapsto t]\bigr)\Big|{t=x\mu} = -\sin(k\cdot x),k_\mu,$$
using phase_update_self to restore the evaluation point. Multiply through by the constant $c$ via const_mul, unfold the definition of $\partial_\mu$, and finish with ring.
why it matters
This is the first nontrivial differentiation step that carries the real-cosine convention into the continuum answer. Downstream, linChristoffel_eq applies it three times to show that the linearized Christoffel symbol of a cosine metric wave is a pure sine times a $k$- and $H$-dependent amplitude:
$$\Gamma^{(1)}{\lambda\mu\nu} = \mathrm{chrAmp}(H,k){\lambda\mu\nu},\sin(k\cdot x).$$
That identity is the bridge from the classical A1 formula $\Gamma^{(1)}{\lambda\mu\nu}=\tfrac12(\partial\mu h_{\lambda\nu}+\partial_\nu h_{\lambda\mu}-\partial_\lambda h_{\mu\nu})$ into the second-variation computation that independently produces the continuum TT coefficient. The module exists precisely to derive that number without reading the Regge side, closing the gap left by the underived discreteBookkeepingFactor := 2 in the older norm gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.