e_213003
plain-language theorem explainer
For the six-index tuple (2,1,3,0,0,3) on Fin 4, the folded Regge numerator coupling m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic decide-cell in the 256-case kernel that builds the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,3,0,0,3)$ with each index in $\{0,1,2,3\}$, the folded numerator coupling $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 are compared. The numerator map $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each tuple. The comparison target is an explicit piecewise integer kernel $Z$ (explicitZ), tabulated by pattern-matching on the six indices (sample values include $4$, $-2$, and so on).
The local module is chunk 9 of a 256-cell decide grid that discharges one concrete multi-index at a time. The theoretical setting is the exact midpoint $M_2$ TT identity in 4D Regge calculus: the claim that the folded numerator is identically eight times the explicit kernel on every index tuple.
Upstream, both $m_2^{\mathrm{num}}$ and $Z$ are pure definitions in the kernel-cert module; no analytic hypotheses are carried into this cell.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides on the concrete Fin-4 sextuple $(2,1,3,0,0,3)$, reduces the fold that defines $m_2^{\mathrm{num}}$ and the pattern match that defines $Z$ to integers, and checks equality with $8Z$. No lemmas are invoked beyond the decidable equality of Int.
why it matters
This cell is one of the 256 atomic facts consumed by the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices. That global identity is the algebraic core of the exact midpoint $M_2$ TT certificate in 4D Regge gravity analysis inside the Recognition Science gravity stack.
It does not itself touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder mass formula; it is pure discrete kernel bookkeeping that lets the continuum-facing gravity theorems quote a fully discharged integer identity rather than a sorry or a numeric check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.