e_213103
plain-language theorem explainer
Pointwise certificate that the midpoint M2 TT numerator equals eight times the explicit Z-coupling at multi-index (2,1,3,1,0,3) in (Fin 4)^6. Gravity analysts cite it as one of 256 kernel decides that assemble into the global m2Num = 8·explicitZ identity. Proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,3,1,0,3)$ with each coordinate in $\{0,1,2,3\}$, 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 Regge exact-midpoint analysis for the 4D TT kernel, two integer-valued maps on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums a contribution function over that list at the given multi-index. The companion table $Z$ is an explicit pattern-matched integer function on the same six indices (sample clauses return $4$, $-2$, etc.).
The local module is chunk 9 of a 256-way partition of the kernel: each chunk discharges one concrete multi-index equality $m_2^{\mathrm{num}}=8Z$. The ambient claim is the pointwise identity over all of $(\mathrm{Fin},4)^6$, later assembled by exhaustive case split.
proof idea
Both sides are closed integer expressions once the six Fin-4 arguments are fixed to $2,1,3,1,0,3$. The proof is the single tactic decide, which evaluates the fold defining $m_2^{\mathrm{num}}$ and the pattern match defining $Z$, then checks the resulting integer equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by six nested fin_cases sweeps. Each chunk such as this one is a named kernel decide inside that 256-cell cover; without the pointwise facts the global midpoint M2 TT identity has no computational spine.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint discretization of the TT sector, not a forcing-chain step (T0–T8). It closes a finite certificate rather than an open analytic gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.