Wave4
plain-language theorem explainer
Local alias for the 4D continuum wave (metric-perturbation) type used throughout the Euclidean weak-field TT first-variation analysis. Gravity analysts cite it when writing edge-strain, Frobenius pairing, and midpoint-Bloch variation statements without importing the Regge preflight module by name. The body is a pure abbreviation with no proof content.
Claim. Write $\mathrm{Wave}_4$ for the 4D continuum wave type already fixed in the Regge 4D continuum preflight layer (the carrier of Euclidean weak-field TT metric perturbations on the closed midpoint Bloch face).
background
The ambient module studies the genuine cross-term (directional) first variation of the exact midpoint Bloch symbol in the Euclidean weak-field transverse-traceless sector, then transports that variation to the torus-normalized continuum face via the banked continuum limit of the RS action on $H+K$ and $H-K$ plus polarization.
In that setting one needs a fixed carrier type for 4D continuum waves (metric perturbations). The Regge 4D continuum preflight layer already supplies that type; this declaration simply re-exports it under a short local name so sibling lemmas (edge strain, Frobenius pairing, coupling weights, exact midpoint Bloch first variation) can refer to it uniformly.
The module honesty block restricts all theorems here to the Euclidean weak-field TT sector of the closed midpoint Bloch continuum face: not a source equation, not Ricci/null focusing, and not GAP1 closure.
proof idea
Pure abbreviation: one-line alias of the preflight continuum wave type. No tactics, no lemmas, no proof obligations.
why it matters
Gives the gravity analysis module a stable local name for the 4D TT wave carrier without threading the full Regge preflight path into every signature. Downstream siblings (edge-strain linearity, Frobenius pairing and norm, coupling-weight cross terms, and the exact midpoint Bloch first variation) are written against this alias.
In the broader Recognition chain this sits inside the continuum face that later must be matched, via a Recognition-derived Freudenthal exact-$J$ metric refinement, to sourced response and Lorentzian null-dyad Ricci/stress transport. The present declaration itself only names the wave type; it does not close that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.