phase_update_self
plain-language theorem explainer
Updating a spacetime coordinate with its own value leaves the plane-wave phase k·x unchanged. Anyone differentiating real cosine or sine waves along a coordinate axis cites this identity. The proof is a one-line simp: Function.update at the current value is the identity map.
Claim. For wavevector $k$ and point $x$ in $\mathbb{R}^4$, and any coordinate index $\mu\in\{0,1,2,3\}$, the plane-wave phase satisfies $k\cdot(\mathrm{update}\,x\,\mu\,(x_\mu))=k\cdot x$.
background
This module derives the continuum transverse-traceless second variation of $\int R\sqrt{g}$ in 4D from the linearized Levi-Civita connection alone, matching the 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 Euclidean dot product $\mathrm{phase}(k,x)=\sum_i k_i x_i$.
Partial derivatives of scalar fields are taken by freezing all but one coordinate and differentiating in that slot. That construction uses Function.update, so one needs that writing the current value back into slot $\mu$ does not move the point, and therefore does not change the phase. The identity is the base case before chain-rule applications to $\cos(k\cdot x)$ and $\sin(k\cdot x)$.
proof idea
Term-mode proof reduced to a single simp. Lean’s definition of Function.update returns the original function whenever the written value equals the existing coordinate, so update x μ (x μ) = x definitionally; applying phase k to both sides yields equality. No external lemmas are required.
why it matters
Feeds the two derivative identities pd_cos and pd_sin, which the module doc flags as the step that carries the real-standing-wave convention into the continuum answer. Those derivatives enter the linearized Christoffel symbols and the second variation of the Einstein-Hilbert integrand on a real TT plane wave. Without this identity the chain-rule proofs would have to re-prove that evaluating the updated phase at the original coordinate recovers $k\cdot x$. The result is local bookkeeping inside Arc 2 step 7; it does not itself force $D=3$ or the eight-tick structure, but it sits in the 4D continuum calculation that is later compared to the discrete Regge Hessian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.