e_022032
plain-language theorem explainer
For the six-index slot (0,2,2,0,3,2) on Fin 4, the folded numerator coupling equals eight times the explicit integer kernel value. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one decided cell. The proof is a single kernel `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,0,3,2)$ in $\mathrm{Fin}\,4$, the folded numerator coupling $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 2 of a 256-cell kernel certification that the folded numerator coupling equals eight times an explicit integer table on every six-tuple in $(\mathrm{Fin},4)^6$. The local setting is the 4D Regge midpoint analysis of the M2–TT identity in the Gravity stack.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a contribution map over a fixed coupling list: start at $0$ and add each term's contribution at the six indices. The explicit kernel $Z$ is a piecewise integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on distinguished patterns).
The parent assembly theorem states the identity for all indices and discharges it by exhaustive fin_cases. Each chunk theorem such as this one pins one concrete cell so the kernel can decide equality of two closed integer expressions.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six indices are substituted into the fold definition of the numerator and the piecewise definition of the explicit kernel; the decision procedure checks the resulting integer equality.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts the identity for every six-tuple in $(\mathrm{Fin},4)^6$ and proves it by nested fin_cases on all six arguments. That universal equality is the algebraic backbone of the Regge-exact midpoint M2–TT identity in 4D within the Gravity analysis path.
In the broader Recognition Science gravity program, certifying that the folded coupling numerator is exactly eight times a sparse explicit kernel removes a large case-bash from later curvature and continuum-limit arguments. This cell is one of 256 decided instances; together they close the numerator side of the identity without leaving residual sorrys on the integer table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.