e_202012
plain-language theorem explainer
At multi-index (2,0,2,0,1,2) on (Fin 4)^6, the folded Regge coupling numerator equals eight times the explicit integer table. Gravity analysts cite it as one of 256 kernel point checks for the 4D midpoint M2 TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,2,0,1,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer table entry: $N(2,0,2,0,1,2)=8\,Z(2,0,2,0,1,2)$.
background
This module is chunk 8 of a 256-point kernel certification that the 4D Regge midpoint M2 TT numerator matches an explicit closed form. The ambient setting is discrete gravity on a 4-simplex skeleton: couplings are tabulated over six Fin-4 indices and reduced by exact integer arithmetic.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list, accumulating each term's contribution at the six indices. The comparison target $Z=\mathrm{explicitZ}$ is a sparse integer table on $(\mathrm{Fin},4)^6$ (typical nonzero values $\pm 2,,4$). The local claim is the scalar identity $N=8Z$ at one concrete sextuple.
Upstream, both $N$ and $Z$ live in the kernel certificate module; the full quantified statement is assembled by exhausting all Fin-4 cases.
proof idea
One-line computational proof: decide evaluates both sides at the fixed Fin-4 sextuple $(2,0,2,0,1,2)$ and checks integer equality. No lemmas are invoked beyond the kernel's evaluation of the fold defining the numerator and the match table defining the explicit form.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,, N=8Z$ by exhaustive fin_cases. Each chunk such as this one discharges one of the 256 kernel points so the quantified identity is a pure case split rather than an open computation.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2 TT relation in 4D Regge calculus: once numerator and explicit table agree everywhere, downstream curvature and deficit identities can quote a closed integer form instead of a fold. It does not itself touch the T0–T8 forcing chain or the J-cost; it is infrastructure inside the discrete gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.