e_112010
plain-language theorem explainer
For the six-index slot (1,1,2,0,1,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}1$, $b{=}1$, $c{=}2$, $d{=}0$, $i{=}1$, $j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator $N_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 5 of a 256-case kernel certification that the Regge midpoint $M_2$ numerator equals eight times an explicit integer table on six $\mathrm{Fin},4$ indices. The local setting is pure finite enumeration: every index runs over ${0,1,2,3}$.
The numerator $N_2$ (Lean m2Num) is defined by folding a fixed coupling list and summing a contribution at each term for the six indices. The explicit kernel $Z$ (Lean explicitZ) is a pattern-matched integer table on those same six indices (sample values include $4$, $-2$, and so on). The claim is the pointwise equality $N_2 = 8Z$ at one concrete six-tuple.
Upstream, both $N_2$ and $Z$ live in the kernel-cert module; this chunk only discharges one decide instance of the equality.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides as concrete integers (the fold defining $N_2$ at $(1,1,2,0,1,0)$ and eight times the table lookup for $Z$ at the same indices) and checks equality by computation. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N_2=8Z$ by exhaustive fin_cases over all six $\mathrm{Fin},4$ arguments. Each chunk theorem such as this one is a leaf of that case split: the assembler reduces to 256 concrete equalities, and this declaration is the leaf for indices $(1,1,2,0,1,0)$.
In the gravity analysis stack, the identity $N_2=8Z$ is the certified algebraic core of the Regge exact-midpoint $M_2$ TT identity in 4D. Closing every chunk removes scaffolding from that identity and lets downstream curvature or continuum-limit arguments quote a fully decided finite kernel rather than an open fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.