e_012301
plain-language theorem explainer
Pointwise identity: the 4D Regge midpoint coupling numerator at index tuple (0,1,2,3,0,1) equals eight times the explicit integer kernel at those indices. Gravity analysts cite it as one cell of the 256-case kernel certificate. The proof is a single kernel decide.
Claim. For indices $(a,b,c,d,i,j)=(0,1,2,3,0,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals $8$ times the explicit integer kernel value at the same indices.
background
This module is chunk 1 of the 256 kernel decides that certify the 4D Regge exact-midpoint identity equating the coupling numerator to eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. the four spacetime directions.
The numerator m2Num is defined by folding a fixed coupling list: it sums a contribution function over that list at the six indices. The comparison target explicitZ is a closed-form integer table on $(\mathrm{Fin},4)^6$, with sample entries such as $4$ on diagonal-type patterns and $-2$ on mixed patterns.
Local goal of the chunk: discharge one concrete sextuple so the assembly theorem can quote the full pointwise equality.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(0,1,2,3,0,1)$ and checks integer equality. No lemmas are invoked beyond the definitions of the numerator fold and the explicit kernel table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhausting cases. That global equality is the algebraic core of the 4D Regge exact-midpoint $M_2$ TT identity certificate in the Gravity analysis stack.
In the Recognition framework this sits inside the discrete gravity / Regge side of the forcing story (spatial $D=3$ plus time, eight-tick structure upstream), converting a summed coupling expression into a sparse explicit integer kernel. The chunking into 256 decide cells keeps each certificate tiny and machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.