e_110203
plain-language theorem explainer
For the six Fin-4 indices (1,1,0,2,0,3), the summed Regge coupling numerator equals eight times the explicit integer kernel at that multi-index. Gravity analysts cite it as one atomic case in the 4D midpoint M2–TT identity. The proof is a pure kernel decision: Lean evaluates both sides and checks equality.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(1,1,0,2,0,3)$. Then the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the exhaustive verification that the 4D Regge midpoint numerator coincides with eight times a closed-form integer kernel. The ambient setting is the exact midpoint M2–TT identity for discrete gravity: every multi-index in $(\mathrm{Fin},4)^6$ must satisfy the same numerical relation.
The numerator $N$ is defined by folding a fixed coupling list: start at $0$ and add a contribution for each coupling term at the six indices. The explicit kernel $Z$ is a pattern-matched integer table on those same six indices (typical nonzero entries are $\pm 2,\pm 4$). Both live in the kernel-certificate module imported here.
Chunk 5 packages 256 such pointwise equalities so the global assembler can discharge the universal statement by case split rather than by a single giant computation.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six concrete Fin 4 arguments are substituted, so the kernel evaluates $N(1,1,0,2,0,3)$ and $8\cdot Z(1,1,0,2,0,3)$ and confirms they match. No lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j,, N=8Z$ by nested fin_cases over all six indices. Each chunk lemma such as this one closes one concrete cell of that $4^6$ grid.
In the Recognition gravity stack this identity is infrastructure for the exact midpoint form of the discrete Einstein–Regge calculus in four dimensions: it replaces an opaque summed coupling by a sparse explicit integer kernel, which is what later curvature and continuum-limit arguments consume. It does not itself touch the forcing chain (T0–T8) or the J-cost; it is pure discrete-gravity algebra supporting those higher layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.