e_000321
plain-language theorem explainer
For the six-index tuple (0,0,0,3,2,1) on Fin 4, the midpoint Regge numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite these atomic equalities when assembling the global identity m2Num = 8·explicitZ over all 4^6 index combinations. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=c=0$, $d=3$, $i=2$, $j=1$ in $\mathrm{Fin}\,4$, the folded 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 local contributions at each multi-index. The comparison target explicitZ is a sparse pattern-matched integer table (typical nonzero values $\pm 2,4$) encoding the closed-form midpoint kernel.
The module is one chunk of the 256-case decide lattice that discharges $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. Chunk 0 covers a block of concrete index sextuples; each theorem pins one sextuple so the assembler can recombine them by exhaustive fin_cases.
No continuum curvature or continuum limit is at stake here: only exact integer arithmetic on the discrete kernel.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides of $m_2^{\mathrm{num}}(0,0,0,3,2,1)=8\cdot Z(0,0,0,3,2,1)$ as concrete integers (the fold over couplingZList versus the pattern match in explicitZ) and accepts the equality by computation. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in Fin 4 by fin_cases and invokes each chunk equality such as this one. That global identity is the algebraic backbone of the exact midpoint M2TT identity in the 4D Regge gravity analysis: it certifies that the folded coupling numerator is precisely eight copies of the closed-form kernel, with no residual defect on the discrete index set.
Within Recognition Science gravity work this is bookkeeping infrastructure rather than a forcing-chain landmark (T0–T8). It closes a finite computational obligation so higher layers can treat $m_2^{\mathrm{num}}=8Z$ as an unconditional fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.