Wave4
plain-language theorem explainer
Wave4 is the type of real 4-component fields on Fin 4, i.e. discrete amplitudes or mode coefficients in the 4D Regge–Bloch edge analysis. Anyone citing the edge-origin m² certificates or seed-edge contribution maps uses this as the ambient space for those vectors. The declaration is a one-line type synonym with no proof content.
Claim. Write $\mathrm{Wave}_4$ for the space of real-valued maps on a 4-element index set, equivalently $\mathbb{R}^4$ with coordinates labeled by $\{0,1,2,3\}$.
background
The module certifies edge-origin second-moment evaluations on the TT / symbolDir sector of the 4D Regge–Bloch analysis. The target identities are that the all-orbit distinct-hinge edge-origin moments equal $-1/4$ on both the plus and cross TT axes, with an explicit orbit slice (t11 = -3, t12 = t21 = t31 = t22 = 0, t13 = 3/2) that reduces to $-3/6 + (3/2)/6 = -1/4$. Integer certificates run by radical-cancelled decide over Fin 24 × Fin 10.
Wave4 is the ambient real 4-vector type for those mode coefficients and for the seed-edge contribution maps that feed the moment assembly. Upstream, the gluing derivation supplies a minimal single-edge complex (two vertices, one edge) used as the combinatorial seed for edge-origin contributions. Sibling abbreviations (Mat4, SeedEdgeContribZ, toReal12/13/22) package the integer and real matrix data that evaluate against Wave4-valued inputs.
proof idea
Pure abbreviation: Wave4 is defined as Fin 4 → ℝ. No lemmas, tactics, or computational content; it is a type synonym so later maps and certificates can name 4-component real amplitudes uniformly.
why it matters
In the gravity analysis stack this type is the carrier for discrete wave / mode data on the 4D edge-origin fold-repair certificates. The module closes the distinct-hinge edge-origin m² moment on TT/symbolDir at -1/4 and rules out pure-gauge counterexamples (gaugePart (1,1,0,0) e₂ and decoyGauge on symbolDir). Wave4 itself is not a physical claim; it is the naming layer those certificates and the seed-edge contribution lemmas sit on. It does not touch gap_action_recovery, base0, or covering-permutation arguments, which the module explicitly forbids. No downstream used_by edges are recorded yet; the type is local scaffolding for the integer and real evaluation lemmas in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.