e_101300
plain-language theorem explainer
For the six-index slot (1,0,1,3,0,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over all 4^6 index tuples. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling sum $m_2^{\mathrm{num}}(1,0,1,3,0,0)$ equals $8$ times the explicit integer kernel $Z(1,0,1,3,0,0)$.
background
This module is chunk 4 of a 256-way case split proving that the Regge midpoint numerator equals eight times an explicit integer table on six Fin-4 indices. The ambient setting is 4D discrete gravity analysis: couplings are summed into a numerator that should match a closed kernel used in the midpoint M2/TT identity.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and adding each contribution at those indices. The comparison target explicitZ is a pattern-matched Int-valued table on the same six indices (sample clauses include values such as $4$, $-2$, and further sparse nonzero entries).
Chunk theorems pin one concrete six-tuple at a time so the assembler can recombine them by exhaustive fin_cases without re-deciding the whole kernel in one go.
proof idea
One-line decide on the ground instance. Both sides reduce to concrete integers: the left by evaluating the fold of coupling contributions at $(1,0,1,3,0,0)$, the right by looking up $8\cdot Z(1,0,1,3,0,0)$ in the explicit table. No lemmas beyond kernel computation are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z$ and discharges the claim by nested fin_cases over all six Fin-4 arguments, each leaf hitting a chunk identity of this form.
In the Recognition gravity stack these numerator identities certify the discrete midpoint curvature bookkeeping that underpins exact 4D Regge/TT comparisons. The module doc frames the whole family as "m2Num = 8·explicitZ, chunk 4 (256 kernel decides)"; this entry is one of those decides. It does not itself touch the T0–T8 forcing chain, but it is infrastructure for the gravity side of the monolith once the geometric dimension $D=3$ spatial (T8) and discrete tick structure are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.