e_302302
plain-language theorem explainer
For multi-index (3,0,2,3,0,2), the folded midpoint M2 coupling numerator equals eight times the explicit integer kernel Z. Gravity analysts assembling the exact 4D Regge midpoint TT identity cite this as one decided kernel case among the chunked 256. Proof is a single kernel `decide` on concrete integer equality.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(3,0,2,3,0,2)=8\,Z(3,0,2,3,0,2)$, where $Z$ is the explicit integer kernel table.
background
This module sits in the Gravity analysis stack for the exact Regge midpoint M2 TT identity in 4D. The local goal, per the module header, is to certify $m_2^{\mathrm{num}}=8\cdot Z$ case-by-case (chunk 12 of the 256 kernel decides).
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a contribution function over a fixed coupling list: start at 0 and add each term's contribution at the six Fin-4 indices. The explicit kernel $Z$ is a pattern-matched integer table on the same six indices (sample entries include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both objects live in the KernelCert module; this chunk only evaluates one concrete six-tuple.
proof idea
One-line kernel proof: decide. Both sides reduce to closed integer expressions (the fold of m2Num at fixed indices versus eight times the matched explicitZ entry), so the decidable equality on Int closes the goal with no lemmas or case splits inside this declaration.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which asserts the identity for every six-tuple in $(\mathrm{Fin},4)^6$ and discharges the universal claim by exhaustive fin_cases on the six indices. Each chunk theorem such as this one supplies a concrete cell of that case tree.
In the broader Recognition gravity stack, the midpoint M2 TT identity is part of the exact discrete curvature bookkeeping that underpins continuum limits and effective Newtonian response. Closing the numerator-versus-kernel relation removes a scaffolding gap in that identity; it does not itself invoke the forcing chain (T5–T8) or the RCL, but it is infrastructure those continuum claims rely on once the discrete kernel is trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.