e_131011
plain-language theorem explainer
For the six-index tuple (1,3,1,0,1,1) on Fin 4, the folded Regge numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D midpoint M2–TT identity. The proof is a single decide, evaluating both integer sides in the kernel.
Claim. For indices $(a,b,c,d,i,j)=(1,3,1,0,1,1)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(1,3,1,0,1,1)=8\,Z_{\mathrm{ex}}(1,3,1,0,1,1)$.
background
This module is chunk 7 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{ex}}$ on all six-tuples of Fin 4 indices. The setting is the exact midpoint M2–TT identity for 4D Regge calculus in the Recognition gravity stack.
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 those indices. The comparison object $Z_{\mathrm{ex}}$ is an explicit integer-valued kernel on the same six indices, tabulated by pattern (e.g. diagonal blocks map to 4, certain off-diagonal pairs to $-2$).
Both sides are pure integers, so each fixed tuple is a finite decision problem. Upstream definitions live in the KernelCert module; this chunk only pins one concrete multi-index.
proof idea
One-line computational proof: by decide. Lean reduces both m2Num 1 3 1 0 1 1 (the fold over the coupling list) and 8 * explicitZ 1 3 1 0 1 1 (lookup in the explicit kernel table, scaled by 8) to concrete integers and checks equality. No lemmas are invoked beyond the decidable equality of Int.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 six-tuple into the global identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ by exhaustive fin_cases. This declaration discharges the single cell $(1,3,1,0,1,1)$ inside that grid (chunk 7 of the 256 kernel decides).
In the Recognition gravity analysis, the identity certifies that the folded midpoint numerator matches the closed-form kernel used in the 4D Regge M2–TT exactness argument. Without the cell-by-cell match, the assembly theorem cannot close, and the exact midpoint identity stays conditional on unchecked index combinations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.