e_312102
plain-language theorem explainer
For the Fin-4 index sextuple (3,1,2,1,0,2), the folded midpoint M2 numerator equals eight times the explicit integer Z-kernel. Gravity analysts certifying the 4D Regge exact midpoint TT identity cite it as one decided cell in chunk 13. Proof is a single kernel `decide` on concrete integers.
Claim. With indices $a=3$, $b=1$, $c=2$, $d=1$, $i=0$, $j=2$ in $\{0,1,2,3\}$, the coupling-fold numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel on six Fin-4 arguments.
background
This module sits in the 4D Regge gravity analysis that certifies an exact midpoint M2 TT identity. The local goal, per the module header, is to prove $m_2^{\mathrm{num}}=8\cdot Z$ by chunked kernel decisions (chunk 13, 256 decides).
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of couplingZList under a contribution map: it sums integer edge/coupling terms at the six Fin-4 indices. The explicit kernel $Z$ is a pattern-matched integer table on the same six indices (sample clauses give values such as $4$, $-2$, and so on).
Upstream, both maps live in the kernel-cert module. Downstream assembly will quantify over all $4^6$ index sextuples; each chunk theorem pins one concrete cell.
proof idea
One-line computational proof: decide. After the six Fin-4 literals are substituted, both sides reduce to closed integer expressions (fold of the coupling list versus a table lookup times eight), and the kernel decides the equality.
why it matters
Parent theorem m2Num_eq_eight_explicitZ asserts $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on the six Fin-4 arguments. This declaration discharges the single cell $(3,1,2,1,0,2)$ inside chunk 13 of that case split.
In the broader Recognition gravity stack, the identity is bookkeeping for the exact midpoint M2 TT kernel in 4D Regge calculus: once every cell matches, the assembled numerator is interchangeable with the closed-form eightfold kernel, which is what later curvature and continuum-matching arguments consume. It does not itself touch the T0–T8 forcing chain, but it is load-bearing scaffolding for the discrete gravity side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.