SRSTTFirstVariation4DCert
plain-language theorem explainer
Certificate packing three facts about the directional first variation of the closed 4D midpoint Bloch symbol: existence of the line derivative at zero strain, the polarization identity relating that derivative to a centered difference, and the continuum TT limit of the torus-normalized variation. Gravity analysts cite it when transporting the Euclidean weak-field TT face toward Einstein–Hilbert. The object is a pure Prop bundle; the companion theorem discharges it by three named lemmas.
Claim. The following three statements hold simultaneously: (i) for all $4\times 4$ matrices $H,K$ and wave covectors $k$, $t\mapsto S(H+tK,k)$ is differentiable at $t=0$ with derivative equal to the exact midpoint Bloch first variation $\delta S(H,K,k)$; (ii) $\delta S(H,K,k)=(S(H+K,k)-S(H-K,k))/2$; (iii) for every nonzero integer mode $m$ and TT matrices $H,K$ relative to $m$, the torus-normalized first variation tends, as the torus side $N\to\infty$, to $-\tfrac14\langle H,K\rangle_F$.
background
The module studies the directional first variation of the closed 4D midpoint Bloch symbol in the Euclidean weak-field transverse-traceless (TT) sector. Algebraic TT means a matrix is symmetric, Euclidean-traceless, and transverse to a given wave covector. Integer modes on the side-$N$ torus supply commensurate wave vectors; the real mode and momentum-norm-squared normalizations convert those into continuum-facing quantities.
The midpoint Bloch symbol is the discrete curvature/action face whose continuum limit is already banked by the closed SRS-to-Einstein–Hilbert convergence theorem. The first-variation object is the genuine cross term obtained by differentiating that symbol along a line of strain matrices. Polarization then recovers the bilinear form from centered differences, so continuum statements proved for $H\pm K$ transport to the mixed pairing.
Upstream cost algebra supplies the shifted cost $H(x)=J(x)+1$ and the Recognition Composition Law in d'Alembert form, but this certificate itself is purely about the Bloch-symbol calculus on Mat4, not about sourcing or null transport.
proof idea
This declaration is a definitional Prop bundle, not a proved theorem. It conjoins three predicates: universal HasDerivAt of the line map $t\mapsto$ exactMidpointBlochSymbol$(H+t\bullet K)$ at $0$; pointwise equality of the first-variation term with the centered difference of the symbol; and Tendsto of the torus-normalized first variation to $-\tfrac14$ times the Frobenius pairing, under nonzero integer mode and TT hypotheses on both strain matrices.
The companion theorem srsTTFirstVariation4D_cert discharges the bundle by packaging three lemmas: the line-derivative lemma, the polarization identity, and the continuum TT first-variation Tendsto obtained from the banked closed SRS–EH convergence on $H+K$ and $H-K$ plus polarization.
why it matters
In the Recognition gravity stack this certificate is the formal interface for the TT directional first variation of the closed 4D midpoint Bloch face. The sole direct consumer is the theorem that proves the bundle, which in turn is the analytic step that turns the banked continuum EH face into a genuine cross-term / bilinear response in the Euclidean weak-field TT sector.
Module honesty is binding: the result is only a theorem in that Euclidean weak-field TT sector. It is not a source equation, not Ricci or null focusing, and not GAP1 closure. The missing future object is a Recognition-derived Freudenthal exact-$J$ metric refinement that would identify the sourced response with this midpoint variation, followed by Lorentzian null-dyad Ricci/stress transport. Do not cite PixelAreaModel, LocalNullPatch, or the model exact-$J$ mesh action as justification here.
Relative to the forcing chain, this sits downstream of continuum Regge/Bloch preflight and the closed SRS–EH Tendsto; it does not itself force $D=3$, $\varphi$, or the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.