Wave4
plain-language theorem explainer
Type alias for real 4-vectors indexed by Fin 4, the ambient space for discrete wave amplitudes in the 4D Regge midpoint analysis. Anyone working the Bloch m² TT identity cites it as the carrier of transverse-traceless mode data. The body is a one-line abbreviation with no proof content.
Claim. Write $\mathrm{Wave}_4$ for the space of real-valued maps on a four-element index set, i.e. $\mathrm{Wave}_4 := \{0,1,2,3\} \to \mathbb{R}$, equivalently $\mathbb{R}^4$.
background
The module closes the exact midpoint Bloch $m^2$ TT identity in four-dimensional Regge calculus (script lineage regge_4d_m2_tt_identity and kernel certs). Discrete gravitational degrees of freedom are packaged as finite-dimensional real arrays; the four-slot index matches the 4D lattice edge or mode labeling used by the flat Hessian Bloch data and edge TT decomposition imports.
Sibling abbreviations in the same file introduce matrix types, Frobenius and wave norms, coupling scalars, and the explicit $m^2$ coefficient assembled from numerator and kernel glue. $\mathrm{Wave}_4$ is the elementary carrier type those constructions act on: a single real amplitude per discrete mode index.
proof idea
Pure definitional abbreviation: identify the name with the function type Fin 4 → ℝ. No lemmas, tactics, or obligations.
why it matters
Gives a stable name to the four-component amplitude space used throughout the midpoint $m^2$ TT identity pipeline. Downstream siblings (waveNormSq, couplingS, m2Coeff, explicit coefficient equalities) read and write these vectors when certifying that the Bloch symbol's TT sector matches the assembled numerator over the kernel. In the broader Recognition gravity stack this is bookkeeping for the 4D Regge analysis that supports continuum limits and mode decompositions; it does not itself encode a physical law, but every identity in the module is typed over it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.