e_112211
plain-language theorem explainer
Pointwise identity: the folded Regge midpoint numerator m2Num at multi-index (1,1,2,2,1,1) equals eight times the tabulated explicit integer explicitZ at the same indices. Gravity analysts assembling the 4D M2TT kernel identity cite this as one of 256 concrete kernel checks. The proof is a single decide on fully concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(1,1,2,2,1,1)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(1,1,2,2,1,1)=8\,Z_{\mathrm{expl}}(1,1,2,2,1,1)$.
background
This module is chunk 5 of a 256-way kernel certification that the Regge exact-midpoint numerator equals eight times a closed-form table. The ambient setting is 4D discrete gravity analysis: six indices each run over $\mathrm{Fin},4$, i.e. coordinate labels ${0,1,2,3}$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling entry. The comparison target $Z_{\mathrm{expl}}$ is an explicit integer-valued case table on the same six $\mathrm{Fin},4$ arguments (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local claim is only the single tuple $(1,1,2,2,1,1)$; sibling declarations cover the other tuples in this chunk.
proof idea
One-line computational discharge: both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed, so decide compares the evaluated fold defining the numerator against $8$ times the matching clause of the explicit table. No algebraic lemmas are invoked beyond kernel evaluation of those two definitions.
why it matters
Feeds the universal assembly theorem $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ for all six $\mathrm{Fin},4$ indices, which is proved by exhaustive case split and consumes these pointwise facts. That identity is the certified algebraic core of the 4D Regge exact-midpoint M2TT kernel used in the gravity analysis stack.
Within Recognition Science this sits in the discrete-gravity / Regge sector that supports continuum limits and effective Newtonian structure; it is bookkeeping infrastructure rather than a T0–T8 forcing step, but the equality must hold exactly for the kernel certificates downstream to be sound. Chunk 5 is one of several parallel decide-batches that close the 256-point table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.