e_020132
plain-language theorem explainer
At multi-index (0,2,0,1,3,2), the folded Regge numerator coupling equals eight times the explicit kernel table entry. Gravity analysts cite it as one of 256 decidable cells in the 4D midpoint M2 identity. The proof is a single kernel decide on concrete Fin 4 indices.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,1,3,2)$ in $\mathrm{Fin}\,4$, the integer numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-cell kernel certification that the folded numerator m2Num agrees with eight times a closed-form table explicitZ on every 4D multi-index. The ambient setting is the exact midpoint identity for the Regge M2 tensor in four dimensions.
m2Num a b c d i j is the integer obtained by folding a fixed coupling list, adding each term's contribution at those six Fin-4 slots. explicitZ is a pattern-matched Int table on the same six indices (sample entries include 4, -2, and so on). The claim is pointwise equality against the scaled table, not a derivation of either definition.
Upstream, both symbols live in the KernelCert module; this file only discharges one concrete cell.
proof idea
One-line computational proof: by decide. After the six Fin-4 indices are substituted, both sides reduce to concrete integers (the fold for m2Num and the match for explicitZ), and Lean's decision procedure checks the equality m2Num 0 2 0 1 3 2 = 8 * explicitZ 0 2 0 1 3 2. No lemmas beyond the two definitions are invoked.
why it matters
The parent theorem is m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 arguments and is assembled by exhaustive fin_cases. Each chunk theorem such as this one supplies a single cell of that 4^6 grid so the assembly can finish without a monolithic decide.
In the gravity stack this underwrites the exact midpoint M2/TT identity used in the Regge analysis path. It is bookkeeping infrastructure rather than a new physical law: once every cell matches, the numerator coupling may be replaced by the compact explicit kernel everywhere downstream. No Recognition forcing-chain step (T5–T8) is proved here; the link is only through the certified 4D Regge kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.