e_010333
plain-language theorem explainer
Pointwise kernel identity: the folded coupling numerator at multi-index (0,1,0,3,3,3) equals eight times the explicit integer Z-table entry there. Gravity analysts cite it as one of 256 decide-chunks that assemble the full 4D midpoint M2 TT numerator identity. The proof is a single kernel decision on concrete Fin-4 integers.
Claim. At the multi-index $(a,b,c,d,i,j)=(0,1,0,3,3,3)$ with each coordinate 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 table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-way kernel split proving $m_2^{\mathrm{num}}=8\cdot Z$ on all $\mathrm{Fin},4$ sextuples for the exact midpoint M2 TT identity in 4D Regge analysis.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at those six indices. The companion table $Z$ is an explicit case-split integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for distinguished index patterns).
The local goal is purely algebraic bookkeeping: check that the fold equals eight times the table at one concrete point, so a later assembler can recombine all points into a universal identity.
proof idea
One-line computational proof: decide evaluates both sides at the closed Fin-4 sextuple $(0,1,0,3,3,3)$ and confirms integer equality. No lemmas are invoked beyond the definitions of the fold numerator and the explicit $Z$ table.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the claim by nested fin_cases over all six indices, routing each concrete cell to a chunk theorem of this form.
In the gravity stack this is infrastructure for the exact midpoint M2 TT identity in 4D Regge calculus: the factor of eight relates the folded coupling numerator to a sparse explicit integer kernel. It does not itself touch the Recognition forcing chain (T5–T8) or the RCL; it is a certified arithmetic tile inside the continuum/Regge analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.