e_311230
plain-language theorem explainer
Pointwise identity: the folded Regge M2 numerator at multi-index (3,1,1,2,3,0) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full 4D midpoint M2–TT numerator identity over all Fin-4 sextuples. The proof is a single kernel `decide` on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,1,2,3,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(3,1,1,2,3,0)=8\,Z(3,1,1,2,3,0)$.
background
In the 4D Regge exact-midpoint M2–TT analysis, two integer-valued kernels on six Fin 4 indices are compared. The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at 0 and add each term's contribution at $(a,b,c,d,i,j)$. The comparison target $Z=\mathrm{explicitZ}$ is an explicit pattern-matched integer table (e.g. $4$, $-2$, and related values on selected index patterns).
This module is chunk 13 of a 256-way partition of the finite index space. The local claim is the scalar identity $N=8Z$ at one concrete sextuple. The ambient goal, stated in the kernel certificate and the assemble module, is the same identity for every $(a,b,c,d,i,j)\in(\mathrm{Fin},4)^6$.
proof idea
Both sides evaluate to concrete Int values once the six indices are fixed. The proof is the one-tactic kernel decision decide, which checks integer equality after unfolding the fold that defines the numerator and the pattern match that defines the explicit table. No algebraic rewriting or intermediate lemmas are required beyond those definitions.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts $\forall a,b,c,d,i,j,, N=8Z$ and discharges the universal quantifier by exhaustive fin_cases on the six indices. Each chunk theorem such as this one supplies (or matches) one decided cell of that $4^6$ table, so the assemble step can close without residual goals.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact midpoint M2–TT identity in 4D Regge calculus, not a forcing-chain landmark (T5–T8). It matters because the closed form $8Z$ is what later curvature and continuum-limit arguments consume; the fold definition alone is too opaque for those steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.