e_312031
plain-language theorem explainer
For the six-index slot (3,1,2,0,3,1) on Fin 4, the folded numerator m2Num equals eight times the tabulated kernel explicitZ. Gravity analysts cite it when assembling the exact midpoint M2–TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(3,1,2,0,3,1)=8\,Z_{\mathrm{ex}}(3,1,2,0,3,1)$, where $Z_{\mathrm{ex}}$ is the explicit integer kernel and $m_2^{\mathrm{num}}$ is the fold of all coupling contributions at that multi-index.
background
This module is one certified chunk of the 4D Regge exact-midpoint M2–TT identity: the claim that the folded numerator m2Num equals eight times a sparse explicit integer table explicitZ at every six-tuple of Fin-4 indices. The module header states the local goal as "m2Num = 8·explicitZ, chunk 13 (256 kernel decides)."
m2Num a b c d i j is defined by folding couplingZList, accumulating each term's contribution at the six indices. explicitZ is a pattern-matched Int-valued kernel on Fin 4^6 (nonzero only on a short list of index patterns such as (0,0,1,1,2,2) ↦ 4). The full identity is the pointwise equality of these two functions.
Chunk theorems pin single multi-indices so the assembler can discharge the universal statement by exhaustive fin_cases without re-running the whole fold in one tactic.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete Fin-4 values (3,1,2,0,3,1) to closed integers and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states ∀ (a b c d i j : Fin 4), m2Num a b c d i j = 8 * explicitZ a b c d i j and proves it by six nested fin_cases, each leaf a chunk such as this one. That universal equality is the algebraic core of the exact midpoint M2–TT identity in the 4D Regge analysis stack.
In the broader Recognition gravity line, the identity constrains discrete curvature/coupling numerators on the eight-tick, D=3 spatial scaffolding; this chunk is pure bookkeeping that closes one of the 4^6 evaluation cells so the identity is machine-checked rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.