e_132002
plain-language theorem explainer
For the six-index slot (1,3,2,0,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this 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=1$, $b=3$, $c=2$, $d=0$, $i=0$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 7 of a 256-case kernel certification that the Regge midpoint $M_2$ numerator equals eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, matching a 4D discrete geometry setting.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling triple at the six indices. The companion table $\mathrm{explicitZ}$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (typical values $\pm 2,,4$, and so on).
The local claim is one concrete six-tuple instance of the identity $m_2^{\mathrm{num}}=8,Z$. The full quantified statement is assembled downstream by exhaustive case split on all six indices.
proof idea
One-line kernel decide. Both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed: the fold that defines $m_2^{\mathrm{num}}$ evaluates, and $\mathrm{explicitZ}$ matches its pattern clause (or default). Lean’s decide closes the resulting integer equality with no further lemmas.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8,\mathrm{explicitZ}$ for all six $\mathrm{Fin},4$ indices, which is the parent used-by edge. That global identity is the algebraic backbone of the Regge exact midpoint $M_2$ TT identity in 4D discrete gravity analysis inside the monolith.
In the Recognition Science gravity stack, certifying the numerator against the explicit kernel table removes a computational gap between the folded coupling definition and the closed form used in continuum or continuum-limit arguments. This chunk is pure bookkeeping: one of 256 decides, not a new physical law, but without it the assembly proof cannot discharge every case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.