phase_update
plain-language theorem explainer
Updating one coordinate of a 4D point shifts the plane-wave phase by the corresponding wave-vector component times the displacement. Anyone differentiating a real cosine wave h(x)=H cos(k·x) under the continuum Einstein-Hilbert second variation cites this identity. The proof is a finite-sum term split: only the updated index contributes, and the rest cancel.
Claim. Let $k,x:\{0,1,2,3\}\to\mathbb{R}$ and fix a coordinate index $\mu$ and a real value $t$. Writing $\mathrm{phase}(k,x)=\sum_i k_i x_i$, one has $\mathrm{phase}\bigl(k,\,x[\mu\mapsto t]\bigr)=\mathrm{phase}(k,x)+k_\mu(t-x_\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 midpoint convention that uses a real cosine wave $h(x)=H\cos(k\cdot x)$.
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=0}^{3} k_i x_i$. Partial derivatives of scalar fields are taken by updating a single coordinate via Function.update, so the first calculus fact needed is how the phase itself responds to that update.
(The unrelated EightTick.phase in the foundation layer is a discrete $k\pi/4$ sampler and is not used here; the local phase is the continuum $k\cdot x$.)
proof idea
Unfold the sum definition of phase. For each index $i$, prove the elementary identity $k_i\cdot(\mathrm{update},x,\mu,t)i=k_i x_i+(\text{if }i=\mu\text{ then }k\mu(t-x_\mu)\text{ else }0)$ by case split on $i=\mu$ versus $i\neq\mu$, using the standard update lemmas and ring. Rewrite the sum by congruence, distribute addition over the finite sum, and simplify: only the $\mu$ term survives.
why it matters
Feeds directly into hasDerivAt_phase_update, which rewrites the coordinate slice of phase as an affine function of $t$ and concludes $\mathrm{HasDerivAt},(\partial_\mu\mathrm{phase})=k_\mu$. That derivative is the seed for all subsequent continuum derivatives of the real TT plane wave under the Einstein-Hilbert integrand.
In the larger Arc 2 program this is bookkeeping for the independent continuum computation that must produce a definite number to compare against the banked Regge Hessian (the frozen preflight $-1/4$ versus the computed $-1/8$, bridged only by an underived factor 2). Non-circularity is structural: the module imports only Mathlib and linear-algebra edge decomposition, never the coupling table or norm gate. No Recognition forcing-chain landmark (T0–T8, RCL, $\phi$) is at stake; the result is classical 4D calculus supporting the continuum side of the discrete/continuum gravity match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.