e_232121
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,3,2,1,2,1) equals eight times the explicit integer kernel at that same index. Gravity analysts assembling the 4D Regge midpoint M2 TT identity cite it as one of 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,b{=}3,c{=}2,d{=}1,i{=}2,j{=}1$ 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 11 of a 256-cell kernel certification that the folded numerator of the 4D Regge midpoint M2 TT identity equals eight times a closed-form integer table. Indices run over $\mathbb{F}_4$ (four discrete directions).
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six indices. The explicit kernel $Z$ is a pattern-matched integer table on those same six $\mathbb{F}_4$ arguments (sample entries include $4$, $-2$, and so on).
The local goal is purely algebraic bookkeeping: check one concrete six-tuple so a later assembly theorem can quantify over all of $(\mathbb{F}_4)^6$.
proof idea
One-line proof by decide. Both sides are closed integer expressions once the six concrete Fin 4 values are substituted: the left folds the coupling list at $(2,3,2,1,2,1)$, the right multiplies the table lookup by eight. Lean’s kernel decision procedure discharges the resulting numeral equality.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk cell such as this one is a leaf of that case tree.
In the Recognition gravity stack this identity is infrastructure for the exact midpoint M2 TT relation in 4D Regge analysis, not a forcing-chain landmark (T5–T8) by itself. It closes one of the 256 discrete cells needed before continuum or continuum-limit arguments can quote a uniform numerator–kernel match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.