e_213110
plain-language theorem explainer
For the six-index slot (2,1,3,1,1,0) in the 4D Regge midpoint kernel, the folded numerator m2Num equals eight times the closed-form explicitZ value. Gravity analysts cite it when discharging one cell of the 256-case identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,3,1,1,0)$ in $\mathrm{Fin}\,4$, the coupling-fold numerator satisfies $m_2^{\mathrm{num}}(2,1,3,1,1,0)=8\,Z_{\mathrm{explicit}}(2,1,3,1,1,0)$.
background
This module is chunk 9 of a 256-cell case split proving that the 4D Regge exact-midpoint M2 TT numerator equals eight times a sparse explicit integer table. The ambient setting is discrete gravity on a 4-simplex skeleton: couplings are summed into an integer numerator before any continuum limit.
m2Num is defined by folding a fixed coupling list and adding each contribution at a six-index slot $(a,b,c,d,i,j)\in(\mathrm{Fin},4)^6$. explicitZ is the matching closed-form table: most slots are zero; a handful of symmetry orbits carry the integers $\pm 2,\pm 4$, etc.
The identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ is the algebraic core of the midpoint M2 TT certificate imported from the KernelCert module. Each chunk theorem pins one concrete multi-index so the assembler can finish by exhaustive fin_cases.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values (the fold for m2Num at this slot, and the pattern-match for explicitZ), and the kernel checks equality. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the universal statement m2Num_eq_eight_explicitZ in the assemble module, which asserts $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ by six nested fin_cases over Fin 4. That universal identity is the numerator half of the Regge exact-midpoint M2 TT certificate in 4D discrete gravity.
Within Recognition Science gravity analysis, the certificate supports exact discrete curvature bookkeeping before continuum or phi-ladder mass formulae are attached. The chunk exists only to keep each decide goal small and machine-checkable; it does not itself touch T5–T8 or the RCL, but it is load-bearing for the 4D Regge kernel used downstream in the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.