e_013203
plain-language theorem explainer
At the six-index point (0,1,3,2,0,3) in (Fin 4)^6, the folded Regge coupling numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it as one atom of the 4D midpoint M2 TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,3,2,0,3)$ with each index in $\{0,1,2,3\}$, 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
The module is one chunk of the 4D Regge exact-midpoint M2 TT 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 (256 points). Local setting: "m2Num = 8·explicitZ, chunk 1 (256 kernel decides)."
m2Num a b c d i j is the integer obtained by folding couplingZList with a contribution map contrib at those indices. explicitZ is the matching sparse table of integers (values such as 4, -2, ...) defined by pattern match on the six Fin-4 arguments. Both live in the kernel-cert module imported here.
This declaration fixes one concrete point of that table, namely (0,1,3,2,0,3).
proof idea
One-line computational proof: by decide. Lean reduces both sides at the literal indices (0,1,3,2,0,3) to concrete integers (the fold for m2Num and the pattern match for explicitZ) and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 indices and is proved by exhaustive fin_cases. Each chunk theorem such as this one discharges one residual goal in that case split (or an equivalent decide grid), so the global numerator–kernel match is only as strong as the full set of 256 pointwise checks.
In the Recognition gravity stack this is bookkeeping for the exact midpoint M2 TT identity in 4D Regge analysis, not a new physical law. It does not itself invoke the forcing chain (T0–T8), RCL, or the phi ladder; it only certifies an integer identity used downstream in the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.