e_113221
plain-language theorem explainer
For the multi-index $(1,1,3,2,2,1)$ on $\mathrm{Fin}\,4$, the folded numerator $m_2^{\mathrm{num}}$ equals eight times the explicit kernel value $Z$. Gravity analysts cite it as one cell of the 256-case exhaustion that upgrades the pointwise kernel certificate to a uniform identity. The proof is a single `decide` on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. For the specific values $a=1$, $b=1$, $c=3$, $d=2$, $i=2$, $j=1$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 5 of a 256-cell kernel certification for a 4D Regge midpoint $M_2$ identity: the claim is $m_2^{\mathrm{num}}=8\cdot Z$ at every sextuple of indices in $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating an integer contribution at each term. The explicit kernel $Z$ is a closed-form integer table on the same six $\mathrm{Fin},4$ arguments (sample entries include $4$, $-2$, and so on for distinguished index patterns).
The local setting is pure finite enumeration: no continuum limit or variational argument appears inside the chunk; each cell only checks one concrete sextuple against the table.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(1,1,3,2,2,1)$ and confirms integer equality. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (the fold) and $Z$ (the explicit table).
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles all 256 cells by nested fin_cases on $(a,b,c,d,i,j)$ and dispatches each residual goal to a chunk equality of this form. Without the pointwise facts, the uniform identity $m_2^{\mathrm{num}}=8Z$ on $\mathrm{Fin},4^6$ does not close.
In the broader gravity analysis, that identity is the algebraic certificate that the midpoint $M_2$ numerator matches eight copies of the explicit kernel, a bookkeeping step inside the Regge-exact 4D midpoint/$TT$ identity development. It does not itself touch the RS forcing chain (T5–T8) or the RCL; it is infrastructure for the discrete gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.