e_310122
plain-language theorem explainer
Pointwise kernel identity: the midpoint M2 numerator at multi-index (3,1,0,1,2,2) equals eight times the explicit Z-table value. Gravity analysts cite it as one cell of the 4D Regge midpoint TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,1,2,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the TT-sector M2 numerator is assembled by folding a fixed coupling list: each term contributes an integer depending on six $\mathrm{Fin},4$ indices, and $m_2^{\mathrm{num}}$ is that fold sum. Parallel to it sits an explicit integer table $Z$ on the same six-index domain, given by a finite case split (e.g. $(0,0,1,1,2,2)\mapsto 4$, mixed pairs $\mapsto -2$).
The local module is chunk 13 of a 256-way kernel partition whose sole job is to certify $m_2^{\mathrm{num}}=8Z$ at each concrete multi-index. The ambient claim is the full identity over all of $(\mathrm{Fin},4)^6$, proved later by exhaustive case split on the six indices.
proof idea
One-line kernel proof: decide evaluates both sides at the fixed tuple $(3,1,0,1,2,2)$ and checks integer equality. No lemmas are invoked; the fold defining the numerator and the case table for $Z$ reduce to concrete Int values that the kernel compares.
why it matters
This cell is consumed by the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the universal quantifier by fin_cases on each index, routing each branch to a chunk identity of this form. Closing the numerator-versus-table match is a necessary algebraic step in the exact 4D Regge midpoint TT identity used in the gravity analysis stack. It does not itself touch the forcing chain (T5–T8) or the RCL; it is pure discrete tensor bookkeeping inside the Regge sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.