e_320122
plain-language theorem explainer
Single kernel case: at index sextuple (3,2,0,1,2,2) the folded coupling numerator equals eight times the explicit integer table. Gravity analysts cite it only as one brick in the 256-case cover of the 4D Regge midpoint M2 TT identity. Proof is a pure `decide` on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,0,1,2,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer table entry: $m_2^{\mathrm{num}}(3,2,0,1,2,2)=8\,Z_{\mathrm{expl}}(3,2,0,1,2,2)$.
background
This module is chunk 14 of a 256-case kernel that certifies the numerator identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ for the 4D Regge exact-midpoint M2 TT analysis. Indices run over $\mathrm{Fin},4$, so the full statement is a finite table check.
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 term's contribution at those six indices. The explicit table $Z_{\mathrm{expl}}$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample clauses include $4$, $-2$, and so on for distinguished index patterns).
The local goal is only the single sextuple $(3,2,0,1,2,2)$. Sibling chunk theorems cover the other concrete points; an assembler later quantifies over all of $(\mathrm{Fin},4)^6$.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed, so the kernel decision procedure closes the equality with no lemmas, rewrites, or case splits inside this declaration.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and discharges the universal claim by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is a named kernel cell in that cover (module doc: "m2Num = 8·explicitZ, chunk 14 (256 kernel decides)").
In the broader Gravity analysis, the identity is bookkeeping for the 4D Regge exact-midpoint M2 TT sector: the folded coupling numerator is replaced by an explicit closed integer table, scaled by eight. It is infrastructure inside the discrete curvature/coupling calculus, not a continuum Einstein-equation derivation and not one of the T0–T8 forcing landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.