Pt
plain-language theorem explainer
Four-dimensional continuum coordinates are modeled as maps from the index set {0,1,2,3} into the reals. Every plane-wave phase, partial derivative, linearized Christoffel amplitude, and Einstein-Hilbert second-variation density in this module is typed over that space. The declaration is a one-line type synonym with no proof content.
Claim. Write $P_t$ for the set of maps $\{0,1,2,3\}\to\mathbb{R}$, i.e. Cartesian 4-coordinates $x=(x^0,x^1,x^2,x^3)$ on the continuum spacetime used for the transverse-traceless second variation of $\int R\sqrt{g}$.
background
This module (Arc 2, step 7) derives, from the Levi-Civita connection alone, the continuum Einstein-Hilbert second variation on a real transverse-traceless plane wave in 4D, in the same convention as the banked Regge midpoint dictionary. It imports only Mathlib and a linear-algebra edge decomposition, so the continuum coefficient cannot have read the discrete answer.
Section 1 introduces coordinates, partials, and the plane wave. The first object is the coordinate type: a point is a 4-tuple of reals, written as a function on Fin 4. The plane-wave phase is then the ordinary dot product $k\cdot x=\sum_{i=0}^{3} k_i x_i$ on that type. Downstream objects (partial derivatives, linearized Christoffel symbols, Frobenius norms of polarizations, and the EH density) all take wavevectors and positions of this type.
The discrete side averages $d^2/dt^2$ of the Regge action under the real cosine wave $h(x)=H\cos(k\cdot x)$. Matching that convention forces the continuum side to work with the same real phase on the same 4D coordinate space.
proof idea
One-line type abbreviation: Pt is defined to be Fin 4 → ℝ. No lemmas, tactics, or obligations.
why it matters
Every nontrivial object in the continuum TT second-variation derivation is parameterized by points and wavevectors of this type. Downstream definitions include the phase $k\cdot x$, the closed-form linearized Christoffel amplitude, the second-variation density, its factorization through phase, the phase-averaged Einstein-Hilbert face $-(1/4),|k|^2|H|_F^2$, and the rigidity theorems that identify that face with the phase average of the density.
The module exists to settle which continuum number the EH action assigns to a real TT plane wave, after the discrete bookkeeping factor of 2 was shown not to be explained by a Frobenius-square normalization. Without a shared 4D coordinate type, the phase average, the density, and the comparison module ReggeNormalizationDerived4D cannot even be stated. The landmark here is D = 3 spatial dimensions plus time (T8), realized concretely as Fin 4 coordinates for the continuum calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.