e_313233
plain-language theorem explainer
For the multi-index (3,1,3,2,3,3) on Fin 4, the folded coupling numerator equals eight times the tabulated explicit kernel integer. Gravity analysts assembling the exact midpoint M2 TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decision (`decide`) on concrete integers.
Claim. For indices $a=3$, $b=1$, $c=3$, $d=2$, $i=3$, $j=3$ in $\mathrm{Fin}\,4$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on sextuples of $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer via a local contribution function, and the fold starts at zero. The explicit kernel $Z$ is a closed-form case table on the same six indices, returning small integers such as $4$, $-2$, and so on.
The module is chunk 13 of a 256-cell partition of the full $\mathrm{Fin},4^6$ domain. Its sole job is to discharge one concrete equality $m_2^{\mathrm{num}}=8Z$ so that a later assembly theorem can recombine all cells by exhaustive fin_cases.
Upstream, both maps live in the kernel certificate module: $Z$ is the pattern-matched table, and $m_2^{\mathrm{num}}$ is the fold definition used uniformly across chunks.
proof idea
One-line kernel proof: decide evaluates both sides on the fixed sextuple $(3,1,3,2,3,3)$ and checks integer equality. No lemmas are invoked; the fold that defines the numerator and the case table that defines $Z$ reduce to concrete Int values that Lean’s decision procedure compares.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by six nested fin_cases, each leaf a chunk equality of this form. This declaration is the leaf for indices $(3,1,3,2,3,3)$.
In the Recognition gravity stack, the exact midpoint M2 TT identity is part of the discrete curvature bookkeeping that must match continuum limits on the eight-tick / $D=3$ side. Closing every kernel cell removes a scaffolding gap in that identity; the factor of eight is the combinatorial normalisation tying the folded coupling list to the explicit $Z$ table.
No open physics claim hangs on this single cell alone; its value is exhaustive coverage inside the assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.