e_312101
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at Fin-4 indices (3,1,2,1,0,1) equals eight times the closed-form integer table entry. Gravity analysts cite it as one cell of the 256-kernel that assembles the global m2Num = 8·explicitZ statement. Proof is a single decide on concrete integers.
Claim. For the index sextuple $(a,b,c,d,i,j)=(3,1,2,1,0,1)$ with each coordinate in $\{0,1,2,3\}$, the summed coupling numerator equals eight times the explicit integer table value: $m_2^{\mathrm{num}}(3,1,2,1,0,1)=8\,Z_{\mathrm{expl}}(3,1,2,1,0,1)$.
background
This module is chunk 13 of a 256-cell kernel certifying that the Regge midpoint $M_2$ numerator matches a closed integer table, entry by entry. The ambient setting is 4D discrete gravity analysis: six indices each run over $\mathrm{Fin},4$, labeling edge/face data in the midpoint scheme.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a local contribution at those indices. The comparison object $Z_{\mathrm{expl}}$ is an explicit pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on). The claim under audit is one concrete sextuple in that table.
Upstream, both $m_2^{\mathrm{num}}$ and $Z_{\mathrm{expl}}$ live in the kernel-cert module; this chunk only evaluates them at fixed indices.
proof idea
One-line computational proof: decide. After substituting the concrete $\mathrm{Fin},4$ literals $(3,1,2,1,0,1)$, both sides reduce to closed integers (the fold on the left, the pattern match on the right), and the kernel decides equality. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
Parent theorem is $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ for all six $\mathrm{Fin},4$ indices, proved by exhaustive fin_cases over the 4^6 kernel. Each chunk theorem such as this one discharges one cell so the assembly stays modular and decidable.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint $M_2$ TT relation in 4D Regge calculus: it converts a summed coupling expression into a sparse closed integer table, which later feeds curvature and continuum-limit comparisons. It does not itself invoke the forcing chain (T0–T8), RCL, or $\varphi$-ladder mass formulae; it is pure discrete-kernel algebra inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.