e_313232
plain-language theorem explainer
One of 256 kernel cases: the folded M2 numerator at index sextuple (3,1,3,2,3,2) equals eight times the explicit Z-coupling table entry. Gravity analysts cite it only as a brick in the full Fin-4 identity m2Num = 8·explicitZ. The proof is a single kernel decide on closed integer arithmetic.
Claim. For the index sextuple $(a,b,c,d,i,j)=(3,1,3,2,3,2)$ with each index in $\mathbb{F}_4$, the folded midpoint $M_2$ numerator equals eight times the explicit integer coupling $Z$ at those indices: $m_2^{\mathrm{num}}(3,1,3,2,3,2)=8\,Z(3,1,3,2,3,2)$.
background
This module is chunk 13 of a 256-case kernel certification that the midpoint $M_2$ numerator in 4D Regge analysis coincides with eight times a sparse explicit coupling table. Indices run over $\mathrm{Fin},4$, i.e. the discrete 4-label set used for simplicial edge/face bookkeeping.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each local contribution at the six indices. The comparison target $\mathrm{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern of integer values (e.g. $\pm 2,,4$ on selected index patterns, and implicitly 0 elsewhere in the match).
The local claim is only the single sextuple $(3,1,3,2,3,2)$. Sibling theorems cover the other tuples; the assemble layer quantifies over all of $\mathrm{Fin},4$.
proof idea
One-line kernel proof: decide. Both sides are closed integer expressions once the six concrete Fin 4 indices are substituted into the fold definition of the numerator and the match definition of explicit $Z$. Lean’s decision procedure evaluates the fold and the table lookup and checks integer equality; no lemmas are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the universal claim by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one concrete case of that split.
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint $M_2$ TT analysis in 4D Regge calculus: it replaces a folded coupling sum by a sparse explicit integer table, which is what later curvature/defect identities actually consume. It does not itself touch the forcing chain (T5–T8), $\phi$-ladder masses, or $\alpha$; it is pure discrete-tensor certification under the gravity analysis modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.