e_313333
plain-language theorem explainer
For the index sextuple (3,1,3,3,3,3) on Fin 4, the folded M2 numerator equals eight times the explicit Z kernel value. Gravity analysts cite it when assembling the pointwise identity m2Num = 8·explicitZ over the full 4^6 grid. The proof is a single kernel decide on that concrete sextuple.
Claim. For indices $a=3$, $b=1$, $c=3$, $d=3$, $i=3$, $j=3$ in $\mathrm{Fin}\,4$, the folded M2 numerator equals $8$ times the explicit integer kernel $Z$ at those indices.
background
In the 4D Regge exact-midpoint M2TT analysis, two integer kernels on six Fin-4 indices are compared. The folded numerator m2Num sums contrib terms over a fixed coupling list. The companion explicitZ is a sparse pattern-matched table of small integers (e.g. 4, -2, ...) on selected sextuples and zero elsewhere.
The module is chunk 13 of a 256-way partition of the kernel: each chunk discharges a block of concrete sextuples so the global identity can be assembled by exhaustive fin_cases. Local setting: prove m2Num = 8·explicitZ pointwise on that block.
proof idea
One-line tactic proof: decide evaluates both sides of the equality at the concrete Fin-4 sextuple (3,1,3,3,3,3) and checks integer equality. No lemmas beyond the definitions of the folded numerator and the explicit Z table are required.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in Fin 4 and is proved by nested fin_cases that ultimately land on these chunk decides. That global equality is the certified algebraic core of the Regge exact-midpoint M2TT identity in the Gravity analysis stack. It is bookkeeping infrastructure rather than a forcing-chain landmark (T0–T8), but without the chunk certificates the 4D midpoint identity does not close in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.