e_232120
plain-language theorem explainer
For the concrete index sextuple (2,3,2,1,2,0) in (Fin 4)^6, the folded Regge midpoint coupling numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one of the 256 kernel cases that assemble the full m2Num = 8·explicitZ identity. The proof is a single decide on the evaluated integers.
Claim. At indices $(a,b,c,d,i,j)=(2,3,2,1,2,0)$ with each coordinate in $\mathbb{F}_4$, 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 11 of a 256-way case split proving the 4D Regge exact-midpoint identity $m_2^{\mathrm{num}}=8\cdot Z$ on the discrete kernel. The ambient setting is discrete gravity analysis: midpoint evaluations of a quadratic coupling built from a fixed list of Z-contributions.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList, accumulating each term's contribution at the six Fin-4 indices. The comparison target explicitZ is a closed integer table on $(\mathrm{Fin},4)^6$, with sparse nonzero pattern (e.g. value 4 on diagonal-type slots, $-2$ on selected off-diagonal slots).
Upstream, both definitions live in the kernel certificate module. The present lemma fixes one concrete sextuple and checks the scalar identity there.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted, so the decision procedure discharges equality with no manual algebra. No named lemmas are invoked beyond the evaluable definitions of the numerator fold and the explicit table.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ and proves it by nested fin_cases on all six indices. Each leaf of that case tree is one of these chunk theorems; this declaration is the leaf for $(2,3,2,1,2,0)$.
In the Recognition gravity stack the identity certifies that the midpoint Regge quadratic form matches an explicit sparse integer kernel, a bookkeeping step toward closed-form curvature and mass-coupling identities. It does not itself invoke the forcing chain (T0–T8), RCL, or the phi-ladder; it is pure discrete-kernel arithmetic supporting those later gravity claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.