e_331012
plain-language theorem explainer
For the concrete index tuple (3,3,1,0,1,2) in Fin 4, the folded Regge coupling numerator equals eight times the tabulated explicit kernel value. Gravity analysts building the 4D midpoint M2 TT identity cite these per-tuple lemmas when assembling the global equality. The proof is a single kernel decide on closed integer arithmetic.
Claim. For $a=3$, $b=3$, $c=1$, $d=0$, $i=1$, $j=2$ in $\{0,1,2,3\}$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel entry at those indices.
background
This module is one chunk of a 256-case kernel certification that the 4D Regge midpoint M2 numerator agrees with eight times an explicit sparse table. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels ${0,1,2,3}$.
The numerator is defined by folding a fixed coupling list: $\mathrm{m2Num}(a,b,c,d,i,j)$ sums $\mathrm{contrib},t,a,b,c,d,i,j$ over every term $t$ in $\mathrm{couplingZList}$. The comparison table $\mathrm{explicitZ}$ is a pattern-matched integer function on six $\mathrm{Fin},4$ arguments, returning a sparse set of values such as $4$, $-2$, and (implicitly) $0$ off the listed patterns.
The local claim is the single six-tuple $(3,3,1,0,1,2)$ inside chunk 15 of that case split.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed, so the kernel closes the equality by evaluation. No algebraic lemmas are invoked beyond the definitions of $\mathrm{m2Num}$ and $\mathrm{explicitZ}$.
why it matters
Parent theorem $\mathrm{m2Num_eq_eight_explicitZ}$ asserts the identity for every six-tuple in $(\mathrm{Fin},4)^6$, proved by exhaustive $\mathrm{fin_cases}$. This declaration discharges one concrete cell of that grid (chunk 15).
In the Recognition gravity stack, the equality $\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ is the certified algebraic core of the Regge exact-midpoint M2 TT identity in 4D. Closing every cell removes a scaffolding obligation on the discrete curvature side of the forcing chain, where $D=3$ spatial dimensions (T8) and the eight-tick octave (T7) already fix the combinatorial skeleton. Without the full case cover, the midpoint identity would remain only a numerical observation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.