meshWave
plain-language theorem explainer
Maps a Recognition Freudenthal 4-mesh and an integer torus mode to the corresponding real wave covector k = 2π m / N on the mesh side. Downstream Hessian and continuum-limit statements cite it as the Bloch wave input. One-line wrapper around the preflight realMode constructor.
Claim. Given a Recognition Freudenthal mesh $M$ with side length $N = N(M)$ and an integer mode $m \in \mathbb{Z}^4$, the mesh wave is the real covector $k \in \mathbb{R}^4$ with components $k_i = 2\pi m_i / N$.
background
This module builds the Recognition gate of the 4D continuum closure: a canonical Recognition mesh on the periodic Freudenthal 4-torus, with a value-level action whose amplitude Hessian is the geometric Option-C midpoint Bloch symbol.
RecognitionFreudenthalMesh4D packages a continuum index $j$; its side is $N = j+3$ (via torusSide). Integer modes IntMode4 are maps $\mathrm{Fin},4 \to \mathbb{Z}$, the commensurate wave vectors on the side-$N$ torus. The preflight constructor realMode N m sends such an $m$ to the real covector $k_i = 2\pi m_i / N$, typed as Wave4.
meshWave is the mesh-native packaging of that conversion: it reads $N$ from the mesh and applies realMode.
proof idea
Pure definitional wrapper. Body is the single application realMode M.side m, so the wave covector is exactly the preflight real mode on the mesh side length. No lemmas or tactics.
why it matters
Supplies the Bloch wave argument for the geometry-derived Option-C midpoint symbol on the Freudenthal mesh. meshTrueReggeQuadraticHessian evaluates exactMidpointBlochSymbol E (meshWave M m), and the closed continuum theorems recognitionExactJConvergesEH_closed and recognitionExactJConvergesGaugeZero_closed thread that Hessian through the discrete torus bridge to the scale-explicit EH and pure-gauge faces.
In the QG campaign this is the value-level carrier link between Recognition mesh data and the Option-C midpoint Bloch analysis. It does not itself close Schläfli elevation or flip gap_action_recovery; those remain open per the module binding notes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.