e_013002
plain-language theorem explainer
For the six-index tuple (0,1,3,0,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic cell in the exhaustive check that the Regge midpoint mass-squared numerator matches the explicit Z table. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}3$, $d{=}0$, $i{=}0$, $j{=}2$ in $\mathrm{Fin}\,4$, the integer $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit six-index kernel table.
background
This module is chunk 1 of a 256-cell kernel certification that the Regge-exact midpoint mass-squared numerator equals eight times an explicit integer table on all six-tuples in $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the given indices. The companion table $Z$ is a pattern-matched integer function on six Fin-4 indices (sample values include $4$, $-2$, and so on for the listed patterns).
The local goal is purely algebraic identity checking: no continuum limit or physical units enter; only that the fold and the table agree up to the constant factor 8 at each concrete multi-index.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are fixed literals, so the kernel evaluates the equality $m_2^{\mathrm{num}}(0,1,3,0,0,2)=8,Z(0,1,3,0,0,2)$ by computation. No lemmas beyond the definitions of the fold and the table are required.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple by exhaustive fin_cases and invokes these chunk cells. That global equality is the certified bridge between the folded coupling definition of the midpoint $m^2$ numerator and the closed-form kernel used in the 4D Regge gravity analysis.
In the Recognition Science gravity stack this is bookkeeping infrastructure, not a forcing-chain landmark (T5–T8). It closes a finite computational obligation so later continuum or continuum-limit arguments can quote a fully decided discrete identity rather than an open fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.