e_312011
plain-language theorem explainer
For the six-index slot (3,1,2,0,1,1) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these pointwise identities when assembling the global m2Num = 8·explicitZ certificate. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=3,b=1,c=2,d=0,i=1,j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local goal, stated in the module header, is to prove $m_2^{\mathrm{num}} = 8\cdot Z$ pointwise by discharging 256 concrete kernel cases.
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 the six Fin-4 indices. The comparison target $Z$ is an explicit integer-valued kernel on the same six indices, tabulated by pattern (e.g. diagonal-type slots map to $4$, crossed slots to $-2$).
Both objects live in the KernelCert layer imported by this chunk. The present declaration fixes one particular six-tuple and asserts numerical equality after the fold.
proof idea
One-line decide proof. Lean evaluates both sides at the concrete Fin-4 sextuple $(3,1,2,0,1,1)$: the fold that defines $m_2^{\mathrm{num}}$ and the pattern match that defines $Z$, then checks the integer equality $m_2^{\mathrm{num}}=8Z$ by computation. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices, routing each cell to a chunk identity of this form.
In the Recognition gravity stack, that global identity is the algebraic backbone of the exact-midpoint Regge $M_2$ TT certificate in 4D: it replaces a folded coupling sum by a closed integer kernel, so curvature and mass-side identities can quote a single explicit table rather than a reduction over the coupling list. Chunk 13 is one of the 256-decide blocks that close the case analysis; without each pointwise fact the assembler cannot finish.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.