Wave4
plain-language theorem explainer
Type synonym for a four-component real field on the discrete index set of size four: maps from Fin 4 into the reals. Used throughout the 4D Regge-normalization arc as the carrier for transverse-traceless wave amplitudes and related axis witnesses. The declaration is a pure abbreviation with no proof content.
Claim. Write $\mathrm{Wave}_4$ for the set of maps $\mathrm{Fin}\,4\to\mathbb{R}$, i.e. ordered 4-tuples of real numbers indexing the components of a 4D wave (or polarization) amplitude.
background
The ambient module compares two second-variation faces of curvature functionals in four dimensions. On the continuum side, the phase average of $d^2/dt^2\int R\sqrt{g}$ per unit volume for a real transverse-traceless cosine wave is $-(1/4),|k|^2,|H|_F^2$, obtained from the Levi-Civita connection alone. On the discrete side sits the Regge action $\sum_h A_h\delta_h$, related to the Einstein-Hilbert integral by an unknown normalization $\rho$.
A four-component real amplitude is the natural carrier for the TT wave $H$ (and for axis witnesses used to pin Frobenius and wave norms). Indexing by $\mathrm{Fin},4$ keeps the discrete bookkeeping finite and matches the 4D spacetime setting of the continuum derivation imported from ContinuumTTSecondVariation4D.
proof idea
Pure type abbreviation: Wave4 is defined to be Fin 4 → ℝ. No lemmas, tactics, or obligations; it is a notational synonym so later equalities (frobSq_eq, momentumSq_eq, waveNormSq_axisWave, dictionary witnesses) can name the amplitude space uniformly.
why it matters
Gives the ambient vector space in which the module measures Regge's normalization constant against the continuum TT second variation. Downstream siblings compare Frobenius and wave norms of axis modes, pin reggeNormalization, and force $\rho=1/2$ (equivalently discreteBookkeepingFactor=2) so the historical $-(1/8)$ vs $-(1/4)$ mismatch is explained as two faces of different actions rather than a failed Regge computation. No direct used_by edges are recorded for the abbrev itself; it is infrastructure for Arc 2 step 7 (second half) and the A4 classical input that $\sum_h A_h\delta_h=\rho\int R\sqrt{g}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.