e_310013
plain-language theorem explainer
For the six-index slot (3,1,0,0,1,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one of the 256 atomic decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,0,0,1,3)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(3,1,0,0,1,3)=8\,Z(3,1,0,0,1,3)$.
background
This module sits in the 4D Regge exact-midpoint analysis of the M2TT identity. The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at a six-tuple of $\mathrm{Fin},4$ indices. The comparison object $Z=\mathrm{explicitZ}$ is a hand-written integer table on the same six indices (typical entries $\pm 2,\pm 4$, with a default branch).
The local setting is chunked verification that $N=8Z$ holds pointwise. Module documentation states the goal as "$\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$, chunk 13 (256 kernel decides)". Sibling theorems cover the other concrete six-tuples; together they feed a single universal statement.
Upstream, $N$ and $Z$ are pure definitions in the kernel-cert module: $N$ is an integer fold, $Z$ is a pattern-matched constant table. No analytic hypothesis is required beyond those definitions.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides at the concrete indices $(3,1,0,0,1,3)$, reduces the fold that defines the numerator and the pattern match that defines the explicit kernel, and checks integer equality. No lemmas are invoked beyond decidable equality on $\mathbb{Z}$.
why it matters
This atom is consumed by the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,,N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ and discharges the universal quantifier by nested fin_cases, routing each concrete cell to its chunk theorem.
In the Recognition gravity stack, the identity certifies that the midpoint Regge M2TT numerator collapses to an explicit sparse kernel (factor eight). That collapse is bookkeeping infrastructure for exact discrete curvature identities in 4D, not a forcing-chain landmark (T5–T8), but it is required scaffolding before continuum or continuum-limit claims can be stated without residual summation error.
Open work sits above the assembler: using $N=8Z$ inside larger Regge or defect-distance arguments rather than re-proving the fold case-by-case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.