e_122001
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (1,2,2,0,0,1) equals eight times the explicit integer table at those indices. Gravity analysts cite it as one kernel cell in the 4D midpoint M2 TT identity. The proof is a single native decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,2,0,0,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit closed-form integer $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling contribution list over those indices: each term adds a local contrib and the accumulator starts at zero. The companion explicitZ is a sparse case table of small integers (entries such as $4$, $-2$, and defaults) meant to be the closed form of that fold divided by eight.
This module is chunk 6 of a 256-cell kernel certification: the module doc states the goal $m_2^{\mathrm{num}}=8\cdot Z$ and discharges it by deciding each concrete sextuple. Upstream definitions live in the KernelCert module; the present file only records one index cell.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel equality is a pure integer check with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhaustive fin_cases. That global equality is the algebraic backbone of the exact midpoint M2 TT identity in the 4D Regge gravity analysis. Each chunk theorem such as this one closes one cell of the 256-way case split so the assembler can finish without sorry. Landmark link is structural (discrete gravity kernel bookkeeping), not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.