e_222031
plain-language theorem explainer
For the six-index tuple (2,2,2,0,3,1) on Fin 4, the folded numerator coupling m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it when assembling the full pointwise identity m2Num = 8·explicitZ over all 4^6 index combinations. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=c=2$, $d=0$, $i=3$, $j=1$ in $\mathrm{Fin}\,4$, the folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices appear. The numerator map $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes via a local contrib and the fold starts at 0. The companion map $Z$ is an explicit case table on the same six indices, returning small integers such as $\pm 2$ or $4$ on the listed patterns (and, by the surrounding cert, the matching values elsewhere).
The local module is chunk 10 of a 256-way split of the kernel identity $m_2^{\mathrm{num}}=8Z$. Each chunk discharges a block of concrete index sextuples so the global assembler can finish by exhaustive fin_cases without a monolithic decide.
proof idea
One-line proof: by decide. Both sides reduce to concrete Int values for the fixed sextuple $(2,2,2,0,3,1)$; the kernel checks equality. No lemmas beyond the definitions of m2Num and explicitZ are invoked.
why it matters
This atom feeds m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,, m_2^{\mathrm{num}}=8Z$ and proves it by nested fin_cases over all six indices, routing each concrete cell to a chunk theorem of this form. Closing the pointwise identity is part of the Regge-exact midpoint $M_2$ TT certification in 4D gravity analysis inside the Recognition Science stack. It does not itself touch the T0–T8 forcing chain, RCL, or the $\phi$-ladder mass formula; it is pure discrete kernel bookkeeping for the gravitational side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.