Wave4
plain-language theorem explainer
Type alias for four-component real vectors indexing plane-wave strain amplitudes on the 4D Freudenthal lattice. Gravity analysts cite it when assembling the exact flat Regge cross-term Hessian on Bloch modes. The body is a one-line abbreviation of Fin 4 → ℝ; no proof content.
Claim. Write $\mathrm{Wave}_4$ for the space of real 4-tuples, i.e. maps $\mathrm{Fin}\,4\to\mathbb{R}$. These are the amplitude vectors for plane-wave class strains in the 4D Regge Hessian analysis.
background
The module studies the exact flat cross-term continuum symbol of the Regge action on the Freudenthal torus. At a flat background, hinge deficits vanish, so the Schläfli identity reduces the second variation to the cross term $S''=\sum_h (dA_h)(d\delta_h)$. That Hessian is evaluated on plane-wave class strains with position-resolved deficit phasing (star-member cube offsets for type-(1,1); per-edge transported origins for the remaining orbits).
Upstream geometry supplies the hinge deficit $2\pi-\sum\theta$ (DihedralAngle / Schläfli). The recognition-ledger deficit is a separate cost sum and is not the geometric object here. Wave amplitudes live in a four-slot real vector because the discrete Bloch analysis is organized over the four coordinate directions of the 4-lattice.
proof idea
Pure abbreviation: Wave4 is defined to be Fin 4 → ℝ. No lemmas, tactics, or wrappers; it is a naming convenience for the four real strain (or mode) components used throughout the module's cube-offset and phased-deficit constructions.
why it matters
Gives a stable name to the amplitude space on which the exact flat cross-term fold and finite Regge symbol act. The module's MODEL tier binds exactFlatCrossTermFold / finiteExactReggeSymbol to geometry-derived flat Hessians on these waves; structural lemmas (homogeneity, zero-momentum drop) and banked $m^2$ certificates for TT/gauge families sit on the same type. Oracle target: normalized TT on axisTTPlus / symbolDir maps to $-1/4$, with vertex-gauge modes annihilated. Open items remain continuum Tendsto for all modes and ledger $S_{RS}$ inhabit; this abbrev only fixes the carrier space. No downstream edges are recorded yet; local siblings (strains, phased-deficit dots, cube offsets) consume it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.