hasDerivAt_finiteExactMidpointBlochSymbol_normalized
plain-language theorem explainer
Along the affine line of strain matrices H + t K, the torus-normalized finite-mesh midpoint Bloch symbol is differentiable at t = 0, with derivative equal to the exact midpoint first variation divided by the mode momentum norm squared. Workers in the Euclidean weak-field TT first-variation pipeline cite this to pass from un-normalized line derivatives to mesh-normalized ones without continuum interchange. The proof applies the un-normalized HasDerivAt lemma and divides by the nonzero constant momentumNormSq.
Claim. Fix a mesh index $j\in\mathbb{N}$, a nonzero integer 4-mode $m$, and matrices $H,K\in M_4(\mathbb{R})$. Let $k_{j,m}$ be the real wave covector of $m$ on the side-$N_j$ torus and write $S_{\mathrm{mid}}(E;k)$ for the exact midpoint Bloch symbol. Then $t\mapsto S_{\mathrm{mid}}(H+tK;\,k_{j,m})/\|k_{j,m}\|^2$ is differentiable at $t=0$, with derivative equal to the exact midpoint first variation $\delta S_{\mathrm{mid}}(H,K;k_{j,m})$ divided by $\|k_{j,m}\|^2$.
background
The module treats the TT directional first variation of the closed 4D midpoint Bloch symbol in the Euclidean weak-field sector. The finite-mesh object finiteExactMidpointBlochSymbol j m E rebinds the continuum exact midpoint Bloch trig-poly to the real mode of the integer wave vector $m$ on the side-$N_j$ torus; it is a comparison/residual specialize route, not the ledger binder.
Normalization is by momentumNormSq of that real mode. The hypothesis $m\neq 0$ guarantees the denominator is nonzero on the torus (via the upstream nonvanishing lemma). Matrices are the 4D Regge continuum-preflight type Mat4. The sibling exactMidpointBlochFirstVariation is the directional cross-term that appears as the target derivative.
Module honesty binds the whole development to the Euclidean weak-field TT sector of the closed midpoint Bloch continuum face: not a source equation, not Ricci/null focusing, and not GAP1 closure.
proof idea
Term-mode, three steps. First invoke momentumNormSq_torus_ne_zero on $(j,m)$ with $m\neq 0$ to obtain a nonzero constant denominator. Second apply the upstream line derivative hasDerivAt_exactMidpointBlochSymbol_line H K (realMode (torusSide j) m), which gives HasDerivAt of $t\mapsto S_{\mathrm{mid}}(H+tK;,k_{j,m})$ at $0$ with value the un-normalized first variation. Third use HasDerivAt.div_const and simpa unfolding finiteExactMidpointBlochSymbol to push the constant division through both the function and the derivative value.
why it matters
This is the normalized finite-mesh directional derivative step (doc-comment: no continuum interchange) inside the TT first-variation pipeline of SRSTTFirstVariation4D. It converts the un-normalized midpoint line derivative into the torus-normalized form that the module later transports, via the banked S_RS_converges_EH_4d_closed Tendsto on $H+K$ and $H-K$ plus polarization, toward the headline continuum face: the torus-normalized midpoint first variation tends to $-\tfrac14$ times the Frobenius pairing.
No downstream consumers are wired yet (used_by empty), so the lemma is presently a local bridge inside this analysis module. Framework-wise it sits in the gravity/Regge continuum preflight layer, not in the T0–T8 forcing chain; the module explicitly forbids citing PixelAreaModel, LocalNullPatch, or the MODEL exact-J mesh action as arguments. The open missing object remains a Recognition-derived Freudenthal exact-J metric refinement identifying sourced response with this midpoint variation, followed by Lorentzian null-dyad Ricci/stress transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.