e_313312
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at Fin-4 indices (3,1,3,3,1,2) equals eight times the explicit integer table. Gravity analysts cite it when assembling the full m2Num = 8·explicitZ kernel. Proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,3,1,2)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local goal, stated in the module header, is to prove $m_2^{\mathrm{num}}=8\cdot Z$ on a block of the $4^6=4096$ index sextuples by discharging 256 concrete kernel goals.
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 a contribution term for each coupling triple. The comparison target $Z$ is an explicit integer-valued table on $(\mathbb{F}_4)^6$, given by pattern match (sample entries include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both definitions live in the kernel certificate module imported here. The present declaration fixes one sextuple in chunk 13 and asserts numerical equality after the fold.
proof idea
One-line computational proof: decide. Lean reduces both sides to concrete integers (the fold over the coupling list on the left, the table lookup on the right) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
Parent assembly theorem m2Num_eq_eight_explicitZ states the universal claim $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges it by exhaustive fin_cases on all six Fin-4 indices. Each chunk lemma such as this one supplies a decided cell of that case tree.
In the broader Gravity analysis, the identity certifies that the folded Regge midpoint numerator agrees with a closed integer form, which is the algebraic backbone of the 4D $M_2$ TT exact-midpoint identity. Without pointwise kernel facts, the assembly cannot close.
No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is directly at stake here; this is pure discrete-gravity bookkeeping inside the Regge sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.