e_001011
plain-language theorem explainer
For the concrete multi-index (0,0,1,0,1,1) on Fin 4, the folded coupling numerator equals eight times the tabulated explicit integer kernel. Gravity analysts cite it when assembling the full m2Num = 8·explicitZ identity over all 4^6 index tuples. The proof is a single kernel decide on the two concrete integers.
Claim. For indices $a=0$, $b=0$, $c=1$, $d=0$, $i=1$, $j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 0 of a 256-way split that certifies, index-by-index, the identity between two integer-valued kernels on six Fin-4 indices. The local setting is the Regge exact-midpoint M2TT analysis in 4D: one side is a fold of coupling contributions, the other an explicit case table.
The numerator m2Num is defined by folding couplingZList and summing each term's contribution at the six indices. The comparison value explicitZ is a total function Fin 4^6 → ℤ given by a finite pattern match (e.g. (0,0,1,1,2,2) ↦ 4, (0,0,1,2,1,2) ↦ −2, and similarly for the remaining tabulated sextuples).
Chunk theorems such as this one pin one concrete sextuple so the assembler can recombine them by exhaustive fin_cases.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted, so the kernel decision procedure closes the equality with no lemmas and no case split inside this declaration.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states ∀ (a b c d i j : Fin 4), m2Num a b c d i j = 8 * explicitZ a b c d i j and proves it by six nested fin_cases that land on the chunk decides (including this one). Without the per-index certificates the assembler cannot discharge the universal claim.
In the gravity stack this identity is bookkeeping for the exact midpoint Regge M2TT kernel in 4D: it equates the folded coupling numerator to eight times the closed-form integer table. It is pure discrete linear algebra on Fin 4, not a continuum GR statement, and sits downstream of the kernel certificate module rather than on the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.