e_320203
plain-language theorem explainer
Concrete index identity: the Regge midpoint numerator at Fin-4 sextuple (3,2,0,2,0,3) equals eight times the explicit kernel integer at those indices. Gravity analysts cite it as one certified cell in the 4^6 case split of the M2TT midpoint identity. The proof is a single kernel decide on closed integer arithmetic.
Claim. For the index sextuple $(3,2,0,2,0,3)\in(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit integer kernel value: $m_2^{\mathrm{num}}(3,2,0,2,0,3)=8\,Z_{\mathrm{expl}}(3,2,0,2,0,3)$.
background
This module is chunk 14 of the certified case table for the 4D Regge exact-midpoint M2TT identity. The local claim is the pointwise relation $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on $\mathrm{Fin},4$ indices, discharged by 256 kernel decides per chunk.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it sums the integer contributions of each coupling term at the six indices. The explicit kernel $Z_{\mathrm{expl}}$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample entries include $4$, $-2$, and other small integers on the diagonal and off-diagonal patterns).
Both definitions live in the kernel-certificate module imported here. The present theorem fixes one concrete sextuple from that table.
proof idea
One-line computational certificate: by decide. Lean reduces both sides of the integer equality (the fold defining the numerator versus eight times the pattern-matched kernel entry) and checks they agree in the kernel. No lemmas are invoked beyond the definitions of the numerator fold and the explicit kernel table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$. That assembly exhausts all sextuples by nested fin_cases; each chunk theorem such as this one supplies a pre-certified cell so the case split stays modular.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint evaluation of the M2TT (second-moment / two-point) sector in 4D Regge calculus. It does not itself invoke the forcing chain (T5 J-uniqueness, T8 $D=3$), but it is part of the certified discrete-gravity substrate those continuum limits sit on. Closing every chunk removes scaffolding from the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.