e_210303
plain-language theorem explainer
For the six-index tuple (2,1,0,3,0,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one cell of the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=1$, $c=0$, $d=3$, $i=0$, $j=3$ in $\{0,1,2,3\}$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each term. The companion map explicitZ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and so on) that is meant to be the closed form of that sum, up to a universal factor of eight.
This module is chunk 9 of a 256-cell decide grid that discharges the pointwise identity $m_2^{\mathrm{num}}=8,Z$ one index tuple at a time. The surrounding certificate module supplies both definitions; the present file only evaluates them at fixed arguments.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six Fin-4 indices are substituted into the fold definition of m2Num and the pattern table for explicitZ, so the kernel closes the equality with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 indices by exhaustive fin_cases and invokes each chunk cell (including this one) as a leaf. That global equality is the algebraic core of the Regge-exact midpoint M2TT identity in 4D gravity analysis inside the monolith. It is bookkeeping infrastructure rather than a forcing-chain landmark (T0–T8), but it locks the discrete curvature numerator to its explicit kernel before continuum or continuum-limit arguments are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.