e_201122
plain-language theorem explainer
For the six-index slot (2,0,1,1,2,2) on Fin 4, the folded M2 numerator equals eight times the explicit kernel value Z. Gravity analysts cite it when discharging one concrete cell of the 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on integer arithmetic.
Claim. For indices $a=2,b=0,c=1,d=1,i=2,j=2$ in $\mathrm{Fin}\,4$, the folded 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 sits in the 4D Regge midpoint analysis of the M2–TT identity. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer weight depending on the six Fin-4 indices $(a,b,c,d,i,j)$, and the fold starts from zero. The companion map $Z_{\mathrm{explicit}}$ is a closed-form integer table on the same six indices (sample values include $4$, $-2$, and so on for the listed patterns).
The local claim of the chunk is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$. The module is one of several decide-chunks that cover the finite index space; the header records that chunk 8 handles a block of the 256 kernel decisions.
proof idea
One-line computational proof: decide evaluates both sides as concrete integers (the fold that defines the numerator versus eight times the table lookup for $Z$) and closes the equality in the kernel. No lemmas beyond the two definitions are required.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ asserts the same identity for every six-tuple in $(\mathrm{Fin},4)^6$. Its proof introduces the six indices and runs fin_cases on each; the present cell is one of the concrete goals discharged along that tree (chunk 8 of the decide grid).
In the broader Recognition gravity stack this identity is bookkeeping for the exact midpoint M2–TT relation in four dimensions: once every index cell matches, the folded coupling numerator is interchangeable with the closed-form kernel, which is the algebraic step needed before continuum or continuum-limit statements. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure finite-index arithmetic supporting the Regge side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.