e_320322
plain-language theorem explainer
For the six-index tuple (3,2,0,3,2,2) on Fin 4, the folded M2 numerator coupling equals eight times the explicit integer Z table at that point. Gravity analysts assembling the 4D Regge midpoint TT identity cite this as one of the 256 kernel cases. The proof is a single kernel decision (`decide`).
Claim. At multi-index $(a,b,c,d,i,j)=(3,2,0,3,2,2)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer lookup table for the 4D midpoint kernel.
background
This module sits in the Gravity analysis stack for the exact midpoint form of the 4D Regge M2 TT identity. The local goal, stated in the module header, is to discharge one chunk of the identity $m_2^{\mathrm{num}}=8\cdot Z$ by kernel decision over the $4^6=4096$ index space, here chunk 14 of the 256-case split.
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 contribution term at the six indices. The comparison table $Z$ is an explicit Fin 4 six-argument integer function with sparse nonzero patterns (e.g. $4$ on paired diagonal blocks, $-2$ on certain off-diagonal swaps).
Both objects live in the kernel certificate module imported here; this file only specializes them to one concrete multi-index and checks equality.
proof idea
One-line proof by decide. Lean reduces both sides at the concrete Fin 4 literals: the fold defining the numerator evaluates to an integer, the explicit $Z$ clause (or default) evaluates to an integer, and the kernel checks $n=8z$. No lemmas are invoked beyond the definitions of the numerator fold and the $Z$ table.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ and proves it by exhaustive fin_cases on each index. Each leaf of that case tree is one of these chunk theorems; this declaration is the leaf for $(3,2,0,3,2,2)$.
In the Recognition gravity stack, the midpoint M2 TT identity is part of the discrete curvature / Regge analysis supporting continuum limits consistent with the forced $D=3$ spatial sector (T8) and the eight-tick causal structure (T7). Closing the numerator-versus-table identity removes a certificate gap in that discrete kernel rather than introducing new continuum physics.
No open scaffold remains on this leaf: the equality is fully decided.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.