explicitM2Coeff
plain-language theorem explainer
Explicit rational m² coefficient table for the 4D midpoint Bloch TT form, indexed by six Fin-4 slots. Gravity analysts proving the exact midpoint Bloch m² identity cite it as the concrete closed coefficient lookup. The body is a one-line alias of the scale-32 integer table cast to ℚ, kept kernel-checkable via the integer certificate.
Claim. For indices $a,b,c,d,i,j \in \{0,1,2,3\}$, the explicit midpoint $m^2$ coefficient is the rational obtained by casting the certified integer table entry at those indices and dividing by $32$.
background
The module closes the exact midpoint Bloch $m^2$ TT identity in 4D Regge analysis: the midpoint Bloch quadratic in a $4\times 4$ hinge matrix $H$ and wave covector $k$ must match a closed bi-quadratic form built from Frobenius, wave, and load norms.
Coefficients of that bi-quadratic are six-index tables on $\mathrm{Fin},4$. The array/Finset sum form m2Coeff is the analytic object; the present definition supplies an explicit rational table meant to equal it entrywise. Upstream, explicitM2CoeffZ is the same table written as $(\mathrm{explicitZ},a,b,c,d,i,j:\mathbb{Q})/32$, replacing a giant match by a scale-32 integer cast that kernel certificates can check.
Local setting is pure discrete gravity analysis (Regge flat Hessian / Bloch data), not the continuum Einstein equation.
proof idea
Definition, not a proof. Body is the one-line alias
explicitM2Coeff := explicitM2CoeffZ,
so every entry is the rational cast of the integer table divided by 32. No tactics; equality to the summed coefficient is deferred to m2Coeff_eq_explicitM2Coeff.
why it matters
Anchors the coefficient side of the midpoint $m^2$ TT identity. Downstream, m2Coeff_eq_explicitM2Coeff equates the summed analytic coefficient to this table; symFull_explicit_eq_symFull_closed matches the fully symmetrized explicit table to the closed coefficient; and exactMidpointBlochM2_eq_closedForm_of_symmetric uses the bi-quadratic with these coefficients to recover the closed form on symmetric $H$.
That chain is what the module header means by closing exact_midpoint_m2_tt_identity (scripts regge_4d_m2_tt_identity_20260721.py and the kernel-cert upgrade). In the broader RS gravity stack it is discrete-analysis scaffolding for Regge TT modes, not a T0–T8 forcing step, but it hardens the 4D midpoint identity used when reading massless TT content off the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.