exactMidpointBlochM2_faces
plain-language theorem explainer
Packages the two exact midpoint Bloch m² Rayleigh faces in 4D Regge analysis: unit-Frobenius TT modes give −1/8, and pure gauge modes give 0. Anyone checking the continuum TT mass identity or residual R3 cites this conjunction. The proof is a one-line pair of the two already-proved face lemmas.
Claim. For every $4\times 4$ real matrix $H$ and wave vector $k\in\mathbb{R}^4$, if $H$ is algebraically TT with respect to $k$ (symmetric, Euclidean-traceless, and transverse), $\|H\|_F^2=1$, and $\|k\|^2\neq 0$, then the exact midpoint Bloch $m^2$ Rayleigh quotient equals $-1/8$. Separately, for every nonzero wave vector $m$ and any $v$, the same Rayleigh quotient on the pure gauge matrix $H_{ij}=m_i v_j+v_i m_j$ equals $0$.
background
This module closes the exact midpoint $m^2$ TT identity for 4D Regge calculus (script-backed continuum preflight). Matrices are Mat4 ($4\times 4$ reals) and waves are Wave4 (maps $\mathrm{Fin},4\to\mathbb{R}$).
Algebraic TT means symmetric, Euclidean-traceless, and transverse to the wave vector. The gauge slice is the rank-at-most-two symmetric matrix $H_{ij}=m_i v_j+v_i m_j$. Frobenius squared norm pins continuum polarization so a fixed coefficient is well-posed; wave-norm squared is the denominator of the Rayleigh quotient.
The quantity exactMidpointBlochM2 is the midpoint Bloch symbol $m^2$ built from the flat Hessian data. The two faces packaged here are the TT eigenvalue $-1/8$ and the gauge null face $0$, which residual R3 consumes as a single conjunction.
proof idea
Term-mode packaging only. The goal is a conjunction, so the proof is the pair constructor applied to the two specialized face theorems already in the module: the TT Rayleigh identity equating the normalized midpoint Bloch $m^2$ to $-1/8$ under IsTT, unit Frobenius norm, and nonzero wave norm; and the gauge Rayleigh identity equating the same quotient on gaugePart m v to $0$ whenever the wave norm is nonzero. No new algebra is performed here.
why it matters
In the 4D Regge continuum preflight, the midpoint Bloch $m^2$ must split cleanly into a fixed TT face and a vanishing gauge face before residual bookkeeping (R3) can certify the continuum TT mass identity. This declaration is the packaged form of that split: it closes exact_midpoint_m2_tt_identity as stated in the module header.
The constant $-1/8$ is the exact continuum coefficient on unit-Frobenius TT polarizations; the gauge face $0$ confirms that pure diffeomorphism directions drop out of the Rayleigh quotient. Downstream residual R3 is the intended consumer (even though the static used-by graph is empty here). Within Recognition gravity analysis this is a local continuum-identity closure, not a forcing-chain (T0–T8) step, but it is required scaffolding for the discrete-to-continuum gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.