e_332011
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at multi-index (3,3,2,0,1,1) equals eight times the explicit integer kernel Z at that same index. Gravity analysts certifying the 4D Regge midpoint TT identity cite it as one of 256 kernel cells. The proof is a single kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,3,2,0,1,1)$ in $(\mathbb{F}_4)^6$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 15 of a 256-cell kernel certification that the folded M2 numerator equals eight times an explicit integer table on all of $(\mathbb{F}_4)^6$. The setting is the 4D Regge exact-midpoint TT identity analysis in the Gravity stack.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each list entry at the six Fin-4 indices. The explicit kernel $Z$ is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a finite case table (sample values include $4$, $-2$, and so on on distinguished index patterns).
The universal claim is assembled downstream by exhausting all six Fin-4 coordinates; each chunk theorem discharges one concrete cell so the assembler need only case-split.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple $(3,3,2,0,1,1)$. The left side reduces by unfolding the fold over the coupling list; the right side multiplies the looked-up table entry by eight. Both sides are closed integer terms, so the kernel closes the equality with no lemmas beyond the two definitions.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathbb{F}_4$, $m_2^{\mathrm{num}}=8Z$, by six nested fin_cases sweeps. Without every cell (this one included), the universal TT-numerator identity does not close.
In the Recognition gravity analysis this is bookkeeping infrastructure for the 4D Regge midpoint mass-squared / TT sector: an exact discrete identity on a finite index set, not a continuum GR derivation. It does not itself invoke the forcing chain (T5–T8), RCL, or the phi ladder; it is a certified arithmetic brick those continuum claims can later rest on once the discrete kernel is fully assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.