finiteExactMidpointBlochSymbolSequence
plain-language theorem explainer
Packages the exact midpoint Bloch trig-poly symbol into a mesh-side sequence for a fixed integer torus mode and 4x4 polarization. Gravity analysts cite it when comparing residual specialize routes against the frozen EH continuum target. The body is a one-line lambda rebinding the pointwise midpoint symbol over the side index.
Claim. For an integer wave mode $m\in\mathbb{Z}^4$ on the side-$N$ 4-torus and a real $4\times 4$ polarization matrix $E$, form the continuum-family sequence $j\mapsto S^{\mathrm{mid}}_j(m,E)\in\mathbb{R}$, where each term is the exact midpoint Bloch symbol of $E$ at the real covector $k=2\pi m/N_j$ on the canonical Freudenthal mesh of side $N_j$.
background
This module is the first binding increment of the 4D Regge continuum closure plan. It freezes the independent weak-field Einstein-Hilbert quadratic target, the canonical periodic Freudenthal 4-torus mesh of side $N\ge 3$, Frobenius-normalized TT data, pure-gauge families, and honesty decoys before any continuum limit is claimed. Nothing in the module proves continuum recovery.
FiniteSymbolSequence is simply $\mathbb{N}\to\mathbb{R}$: a named family of finite-$N$ symbol values indexed by mesh side. Integer modes IntMode4 are commensurate wave vectors $m:\mathrm{Fin},4\to\mathbb{Z}$; the real covector is $k=2\pi m/N$. Polarizations are real $4\times 4$ matrices.
The pointwise building block is the exact midpoint Bloch trig-poly symbol (from the exact flat Hessian Bloch assembly), evaluated at that real mode. Module docs stress this midpoint rebound is a comparison/residual specialize route, not the ledger continuum binder.
proof idea
One-line definitional wrapper. The sequence at index $j$ is definitionally the pointwise exact midpoint Bloch symbol at side index $j$, mode $m$, and polarization $E$. No lemmas are applied; the body is the lambda $j\mapsto$ that pointwise symbol.
why it matters
Sits in the QG full-theory campaign's continuum preflight: it names a concrete mesh-side family built from the exact midpoint Bloch symbol so residual and specialize comparisons can be stated against the frozen EH quadratic without inhabiting the geometric continuum Tendsto props.
Module contracts freeze the EH target independently of lattice weights (no reverse-engineering of scales). After oracle H_fold, the continuum object is the exact flat cross-term symbol, not legacy distinct-hinge transported folds. This midpoint sequence is explicitly tagged comparison/residual, not the ledger binder, and aligns with banked algebraic face bookkeeping rather than geometric recovery.
No downstream uses are wired yet (used_by empty). It supports later discrimination of decoys and status flags while S_RS_converges_EH_4d and gap-action recovery remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.