e_010312
plain-language theorem explainer
For the six-index slot (0,1,0,3,1,2) on Fin 4, the summed coupling numerator equals eight times the explicit integer kernel value at that slot. Gravity analysts cite it when assembling the full pointwise identity m2Num = 8·explicitZ over all 4^6 index tuples. The proof is a single kernel decide on the concrete integers.
Claim. For indices $a{=}0,b{=}1,c{=}0,d{=}3,i{=}1,j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(0,1,0,3,1,2)=8\,Z_{\mathrm{expl}}(0,1,0,3,1,2)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification: the claim that the folded numerator m2Num equals eight times a closed-form integer table explicitZ at every six-tuple of Fin-4 indices. The module doc states the local goal as "m2Num = 8·explicitZ, chunk 1 (256 kernel decides)."
Upstream, m2Num a b c d i j is defined as the fold of contrib over couplingZList, starting from 0. explicitZ is a pattern-matched integer table on six Fin-4 arguments (sample clauses give values such as 4, -2, …). The present declaration fixes one concrete multi-index and equates the two sides there.
Sibling theorems e_010000, e_010001, … cover the other slots in the same chunk; together they feed the exhaustive case split in the assembler.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the equality on the concrete Fin-4 literals to integers (the fold that defines the numerator versus the pattern match that defines the explicit kernel) and checks they match. No lemmas are invoked beyond the kernel decision procedure and the two upstream definitions.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ in the assemble module, which states ∀ six Fin-4 indices, m2Num = 8·explicitZ, proved by nested fin_cases on all six arguments. Each leaf of that case tree is discharged by a chunk theorem of this form; e_010312 is the leaf for (0,1,0,3,1,2).
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2TT kernel in 4D Regge analysis: it replaces a summed coupling expression by an explicit integer table, scaled by 8. It does not itself touch the forcing chain (T0–T8), RCL, or the phi-ladder mass formula; it is infrastructure inside the gravity/Regge certification layer that those higher claims may later consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.