e_012013
plain-language theorem explainer
For the fixed multi-index (0,1,2,0,1,3) on Fin 4, the summed Regge coupling numerator equals eight times the explicit integer kernel entry. Gravity analysts cite it as one atomic case in the 4D midpoint M2 TT identity. The proof is a single kernel decide on two concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(0,1,2,0,1,3)$. Then the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge midpoint analysis of the M2 TT identity. The numerator $N$ (Lean m2Num) is the fold of a fixed coupling list: each term contributes an integer depending on the six Fin-4 indices, and the total is their sum. The explicit kernel $Z$ (Lean explicitZ) is a closed integer table on the same six indices, with sparse nonzero entries such as $\pm 2,\pm 4$.
The local goal, stated in the module header, is to certify $N=8Z$ on a chunk of the $4^6$ index space by kernel decides. Upstream, both $N$ and $Z$ are pure definitions in the kernel-cert module; no analytic hypotheses are attached.
proof idea
Both sides evaluate to concrete integers once the six indices are fixed. The tactic decide asks the kernel to compute $N(0,1,2,0,1,3)$ via the fold and $8\cdot Z(0,1,2,0,1,3)$ from the table, then checks equality. No lemmas beyond the definitions are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 sextuple by nested fin_cases and needs one atomic equality per cell. This declaration discharges the cell $(0,1,2,0,1,3)$. Together the chunk theorems close the numerator-to-kernel identity used in the Regge exact midpoint M2 TT analysis in four dimensions. It is bookkeeping inside the gravity stack, not a forcing-chain landmark (T0–T8), but it is required scaffolding for the discrete curvature identities that feed continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.