e_122111
plain-language theorem explainer
For the six Fin-4 indices (1,2,2,1,1,1), the Regge midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it when assembling the full 4D M2 TT identity over all index tuples. The proof is a single kernel decide on the concrete integers.
Claim. For indices $a=1$, $b=2$, $c=2$, $d=1$, $i=1$, $j=1$ in $\mathrm{Fin}\,4$, the midpoint numerator equals eight times the explicit kernel: $m_2^{\mathrm{num}}(1,2,2,1,1,1)=8\,Z_{\mathrm{ex}}(1,2,2,1,1,1)$.
background
This module is chunk 6 of a 256-case kernel certification that the 4D Regge-exact midpoint numerator equals eight times a closed-form integer kernel. The ambient setting is discrete gravity analysis: verifying an exact algebraic identity for the M2 TT sector at the midpoint of a 4-simplex edge configuration.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those six Fin-4 indices. The explicit kernel $Z_{\mathrm{ex}}$ is a pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on). The claim is the pointwise equality of these two integers at one concrete multi-index.
Upstream, both functions live in the KernelCert module; this chunk only evaluates them at a single tuple.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the equality to concrete integers (the fold that defines the numerator, and the pattern match that defines the explicit kernel) and checks they agree. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts the identity for every six-tuple in $(\mathrm{Fin},4)^6$. Its proof case-splits on all six indices; each leaf is one of these chunk theorems. This declaration discharges the leaf $(1,2,2,1,1,1)$.
In the Recognition gravity stack, the identity is part of the exact midpoint analysis for the 4D Regge M2 TT sector. It is pure discrete-geometry algebra, not a continuum limit statement, and sits downstream of the kernel certification rather than of the T0–T8 forcing chain. Closing all 256 chunks yields the universal equality used by later assembly and gravity-identity modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.