e_133013
plain-language theorem explainer
At multi-index (1,3,3,0,1,3) the Regge midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one of the 256 concrete kernel checks that assemble into the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on fixed Fin-4 arguments.
Claim. For indices $(a,b,c,d,i,j)=(1,3,3,0,1,3)$ with each index in $\{0,1,2,3\}$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 7 of a 256-way split of the 4D Regge exact-midpoint $M_2$ TT-identity kernel. The ambient setting is discrete gravity on a 4-index simplex lattice: one must match a folded coupling sum against a closed-form integer table.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each multi-index $(a,b,c,d,i,j)\in(\mathrm{Fin},4)^6$. The comparison object $\mathrm{explicitZ}$ is a total function on the same domain that returns a sparse integer table (typical nonzero entries are $\pm 2,\pm 4$).
The local claim is the pointwise equality of those two integers at one fixed tuple. Upstream, both sides are pure definitions; no analytic lemma is required beyond evaluating them.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(1,3,3,0,1,3)$ and checks integer equality. No rewriting, induction, or named lemmas are invoked; the kernel certificate is pure decision on closed terms built from m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies over all $(a,b,c,d,i,j):\mathrm{Fin},4$ and discharges the universal statement by exhaustive fin_cases. Each chunk theorem such as this one supplies one case of that cover (module doc: "m2Num = 8·explicitZ, chunk 7 (256 kernel decides)").
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge $M_2$ TT sector in four dimensions: it certifies that the folded coupling numerator is exactly eight times the explicit Z table, so later continuum or continuum-limit arguments can replace the sum by the closed form. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is a discrete algebraic certificate inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.