hasDerivAt_phase_update
plain-language theorem explainer
The plane-wave phase $k\cdot x$ is affine in each coordinate, so its partial along $\mu$ equals the wave-vector component $k_\mu$. Continuum TT second-variation calculations cite this when differentiating real cosine/sine standing waves. The proof rewrites the updated phase via the algebraic update identity, then differentiates the resulting affine map.
Claim. Let $k,x\in\mathbb{R}^4$ and $\mu\in\{0,1,2,3\}$. The real map $t\mapsto k\cdot(x\text{ with }x^\mu\text{ replaced by }t)$ is differentiable at $t=x^\mu$, and its derivative there equals $k_\mu$.
background
This module (Arc 2, step 7) derives the continuum transverse-traceless second variation of $\int R\sqrt{g}$ in 4D from the linearized Levi-Civita connection alone, matched to the discrete Regge real-cosine convention, without importing any banked coefficient.
Coordinates are points $x:\mathrm{Fin},4\to\mathbb{R}$. The plane-wave phase is the ordinary dot product $\mathrm{phase}(k,x)=\sum_i k_i x_i$. The sibling identity phase_update states that replacing the $\mu$-th coordinate of $x$ by a free real $t$ shifts the phase by exactly $k_\mu(t-x^\mu)$.
That algebraic identity is the only upstream input needed here; the EightTick phase name is a separate discrete object and is not used.
proof idea
Pointwise apply the update identity to obtain a function equality: after updating coordinate $\mu$, the phase equals the constant $\mathrm{phase}(k,x)$ plus $k_\mu(t-x^\mu)$. Rewrite the target map by that equality. Differentiate $t\mapsto t-x^\mu$ at $x^\mu$ (identity minus constant), multiply by the constant $k_\mu$, and add the constant phase value. simpa closes the arithmetic.
why it matters
This is the differentiability engine for the real standing-wave convention in the continuum TT calculation. Downstream, pd_cos and pd_sin compose it with Mathlib's cosine and sine derivatives to prove
$\partial_\mu(c\cos(k\cdot x))=-(c k_\mu)\sin(k\cdot x)$ and the sine twin, which the module doc flags as the step that carries the real-cos convention into the answer.
Those partials feed the linearized Christoffel symbols and the second variation of $\int R\sqrt{g}$ under a real TT plane wave, the independent continuum number compared later against the Regge dictionary. No Recognition forcing-chain landmark is at stake; the stake is non-circular derivation of the continuum Hessian coefficient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.