finiteExactMidpointBlochSymbol
plain-language theorem explainer
Finite-mesh evaluation of the exact midpoint Bloch Hessian symbol on the side-(j+3) periodic 4-torus. Sends an integer mode m and a 4×4 matrix E to the unit-cell trig polynomial at k = 2π m / N. Continuum Tendsto binders, normalized first-variation lemmas, and the TT weak-field headline cite this sequence. Pure definitional rebinding of the frozen exact-midpoint symbol onto the preflight mesh family.
Claim. For mesh index $j \in \mathbb{N}$, integer mode $m \in \mathbb{Z}^4$, and $E \in M_4(\mathbb{R})$, return the exact midpoint Bloch symbol of $E$ at the real wave covector $k_i = 2\pi m_i / N$ with torus side $N = j+3$.
background
This module is the Regge 4D continuum preflight: it freezes the weak-field Einstein-Hilbert target, the canonical periodic Freudenthal 4-torus mesh, normalized TT data, and honesty decoys before any continuum recovery is claimed. Nothing here proves Tendsto to EH.
The continuum family uses side length $N = j+3$ (so $N \ge 3$). An integer mode $m : \mathrm{Fin},4 \to \mathbb{Z}$ is converted by realMode to the commensurate covector $k = 2\pi m / N$. Matrices are plain $4\times 4$ real arrays (polarizations or metric perturbations).
Upstream, exactMidpointBlochSymbol is the finite trig polynomial over the unit-cell coupling table: $\sum_i w_i(H),\cos(\phi_i(k))$. The present definition only specializes that symbol to the preflight torus family; the doc tags it as the comparison/residual specialize route, not the ledger binder itself.
proof idea
One-line definitional wrapper. Apply exactMidpointBlochSymbol to the matrix $E$ and to the real wave covector realMode (torusSide j) m, i.e. evaluate the frozen midpoint Bloch trig-poly at $k = 2\pi m/(j+3)$. No tactics, no lemmas beyond the upstream def.
why it matters
Names the concrete finite sequence whose $|k|^2$-normalized Tendsto is the continuum symbol binder. Regge4DContinuumSymbolIs and continuumSymbolIs_iff are literally Tendsto of this quantity over momentumNormSq; finiteExactMidpointBlochSymbolSequence packages it as a FiniteSymbolSequence. Downstream, TorusNormalizedTendsto matches the same mesh object, and the SRS TT first-variation stack uses it both pointwise (hasDerivAt_finiteExactMidpointBlochSymbol_normalized) and in the headline Euclidean weak-field theorem continuumTTFirstVariation_closed (limit $-1/4$ Frobenius pairing on TT).
In the QG campaign this is the geometric mesh sequence for the OPEN continuum target: normalized exact-flat symbol should hit the independently frozen EH coefficient on TT and vanish on pure gauge. Module status still marks Regge4DContinuumEHTarget and S_RS_converges_EH_4d open; this def only freezes the sequence those Props will talk about.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.