e_212303
plain-language theorem explainer
Pointwise identity: the Regge midpoint numerator m2Num at indices (2,1,2,3,0,3) equals eight times the explicit integer kernel explicitZ there. Gravity analysts cite it as one cell of the 256-case kernel that builds the global m2Num = 8·explicitZ theorem. Proof is a single decide on concrete integers.
Claim. For the sextuple of indices $(a,b,c,d,i,j)=(2,1,2,3,0,3)$ with each index in $\mathbb{F}_4$, the folded coupling 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
This module is chunk 9 of a 256-cell kernel certifying $m_2^{\mathrm{num}}=8\cdot Z$ on all sextuples in $(\mathrm{Fin},4)^6$, in the 4D Regge exact-midpoint $M_2$ TT-identity analysis.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at those six indices. The closed form $Z$ is an explicit piecewise integer function on the same six $\mathrm{Fin},4$ arguments (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The local goal is only the single cell $(2,1,2,3,0,3)$; sibling theorems cover the rest of the chunk.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six concrete Fin 4 values are substituted into the fold definition of $m_2^{\mathrm{num}}$ and the pattern-match definition of $Z$, so the kernel equality is a pure Int identity discharged by decision.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk cell such as this one supplies (or is hit by) one branch of that case split.
In the broader Gravity/Regge stack this identity is bookkeeping for the exact midpoint $M_2$ TT kernel in 4D: replacing the folded coupling sum by the explicit $Z$ table makes later curvature and mass-ladder comparisons algebraic rather than combinatorial. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete kernel arithmetic supporting those gravity claims downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.