e_302001
plain-language theorem explainer
For the six-index slot (3,0,2,0,0,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,0,2,0,0,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 12 of a 256-case kernel certification that the Regge midpoint $M_2$ numerator equals eight times an explicit integer table on $(\mathrm{Fin},4)^6$. The local setting is pure finite arithmetic: no continuum limit, only exact integer identities.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums contrib terms over couplingZList for the six indices. The companion table explicitZ is a pattern-matched integer function on the same six Fin 4 arguments (sample values include $4$, $-2$, and so on for the listed patterns).
The chunk theorems pin one concrete sextuple each so the assembler can discharge the universal claim by exhaustive fin_cases.
proof idea
One-line kernel decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are substituted: the left via the fold definition of m2Num, the right via the pattern match in explicitZ (scaled by 8). Lean’s decide closes the resulting integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by six nested fin_cases over Fin 4, routing each cell to a chunk decide such as this one.
In the Recognition gravity stack this identity is the exact midpoint $M_2$ numerator certificate for the 4D Regge analysis: it replaces a symbolic fold by a closed integer kernel, so later curvature and continuum-matching arguments can quote a fully decided algebraic fact rather than an open sum. It is bookkeeping inside the Gravity domain, not a T0–T8 forcing step, but it hardens the discrete-to-continuum bridge those steps rely on when gravity is reconstructed from the recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.