e_320233
plain-language theorem explainer
At multi-index (3,2,0,2,3,3) the folded 4D Regge midpoint numerator m2Num equals eight times the explicit integer kernel table explicitZ. Gravity analysts cite it as one of the 256 concrete kernel checks that assemble the global identity. The proof is a single decide on fully evaluated integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,0,2,3,3)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the given indices. The companion table $Z$ is an explicit pattern-matched integer function on the same six indices (typical nonzero entries are $\pm 2,,4$).
The local module is chunk 14 of a 256-way split of the kernel identity $m_2^{\mathrm{num}}=8Z$. Each chunk discharges a block of concrete index tuples by computation rather than by symbolic algebra. The ambient claim is the pointwise equality of these two kernels on all of $(\mathrm{Fin},4)^6$.
proof idea
One-line computational certificate: both sides are closed integer terms once the six Fin-4 arguments are substituted, so decide evaluates $m_2^{\mathrm{num}}(3,2,0,2,3,3)$ and $8\cdot Z(3,2,0,2,3,3)$ and checks equality. No lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and $Z$ are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on the six indices. Each chunk theorem such as this one is a named kernel point that the case split lands on.
In the Recognition gravity stack this identity is part of the exact midpoint M2/TT analysis in four dimensions: it certifies that the folded coupling numerator is a pure multiple of the explicit Z table, so downstream curvature and mass-squared identities can quote a single closed form. It is pure discrete kernel bookkeeping, not a continuum GR derivation, and sits downstream of the forcing chain only insofar as $D=3$ spatial plus time fixes the 4D index range.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.