phase
plain-language theorem explainer
Defines the real plane-wave phase as the Euclidean four-dot product k·x on R^4. Anyone working the continuum transverse-traceless second variation of the Einstein-Hilbert action cites it as the phase of the real cosine perturbation h(x)=H cos(k·x). The body is the coordinate sum over Fin 4; no lemmas.
Claim. For four-vectors $k,x\in\mathbb{R}^4$, the plane-wave phase is $\varphi(k,x)=k\cdot x=\sum_{i=0}^{3} k_i x_i$.
background
This module (Arc 2, step 7) derives the continuum number that the Einstein-Hilbert action assigns to a real transverse-traceless plane wave, matched to the banked Regge midpoint dictionary. It imports only Mathlib and linear-algebra edge decomposition, so the continuum side is independent of the discrete coupling table and norm gate.
Coordinates are four-vectors: a point type is an abbreviation for maps Fin 4 → ℝ. The discrete Bloch symbol averages the second time derivative of the Regge action under the real wave h(x)=H cos(k·x); the continuum object here is the matching phase average of d²/dt² ∫ R √g per unit volume. The phase is exactly that argument k·x.
Named classical input A1 is the linearized Levi-Civita Christoffel symbol built from partials of h. Downstream siblings (partial derivatives, phase update, wave field, linearized Christoffel) all consume this phase.
proof idea
Pure definition: expand the four-dot product as the finite sum ∑ i : Fin 4, k i * x i. No tactics, no lemmas, no hypotheses.
why it matters
Without a fixed phase convention the continuum TT second variation cannot be compared to the Regge symbol. The module exists precisely because the discrete bookkeeping factor 2 was underived; deriving the continuum side independently requires the same real cosine wave, hence this k·x.
Locally it feeds phase updates, partials of the wave, Frobenius norms, and the linearized Christoffel amplitude that produce the continuum Hessian coefficient. In the broader RS gravity stack it is the continuum counterpart of the eight-tick temporal structure (T7: period 2^3) used when curvature and spatial dimension D=3 are forced. Downstream curvature-space and gauge-counting results reuse phase language when matching continuum and ledger normalizations; the comparison itself lives in ReggeNormalizationDerived4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.