e_313131
plain-language theorem explainer
For the Fin-4 multi-index (3,1,3,1,3,1), the summed Regge coupling numerator equals eight times the explicit integer kernel entry. Gravity analysts cite it as one atomic case in the 4D midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(3,1,3,1,3,1)$. Then the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge midpoint analysis: one proves that a summed numerator built from coupling contributions is identically eight times a sparse explicit integer table on all sextuples in $(\mathrm{Fin},4)^6$.
The numerator $N$ (m2Num) folds a fixed coupling list, adding one integer contribution per term at the six indices. The table $Z$ (explicitZ) is a pattern-matched closed form on those same indices (typical nonzero values $\pm 2,,4$). The module doc frames the work as chunk 13 of 256 kernel decides establishing $N=8Z$ casewise.
Upstream, only the two definitions are needed: the fold that builds $N$ and the case table for $Z$. No analytic lemma is invoked; the equality is pure integer arithmetic at one point.
proof idea
One-line proof: decide. Lean reduces both sides at the concrete indices $(3,1,3,1,3,1)$ to integers and checks equality in the kernel. No lemmas, rewrites, or case splits appear in this declaration itself.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 sextuple into the global identity $N=8Z$ by exhaustive fin_cases. This chunk supplies the single cell $(3,1,3,1,3,1)$ of that grid.
In the gravity stack the identity is bookkeeping for the exact midpoint M2–TT comparison in 4D Regge calculus: once $N=8Z$ is certified everywhere, the analytic side can quote a closed kernel instead of a fold. It is computational scaffolding inside the Gravity domain, not a forcing-chain (T0–T8) step, but it closes one of the 256 decide obligations that make the assembled equality sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.