e_021212
plain-language theorem explainer
For the six-index tuple (0,2,1,2,1,2) in Fin 4, the folded Regge coupling numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts cite it as one atomic case in the exhaustive 4D midpoint M2 identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,2,1,2)$ with each index in $\mathrm{Fin}\,4$, the summed coupling numerator equals eight times the explicit integer kernel entry at those indices: $N(0,2,1,2,1,2)=8\,Z(0,2,1,2,1,2)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $N=\mathrm{m2Num}$ is the fold of a fixed coupling list: it accumulates every local contribution $\mathrm{contrib}$ over $\mathrm{couplingZList}$. The comparison target $Z=\mathrm{explicitZ}$ is a closed-form case table of small integers (entries such as $4$, $-2$, and so on) indexed by the same six-tuple.
The ambient claim of the module family is the pointwise identity $N=8Z$ on all $4^6$ index tuples. This file is chunk 2 of that kernel: it discharges a block of concrete equalities by decision procedure rather than by a symbolic closed form.
Upstream, both $N$ and $Z$ are defined in the KernelCert module; the present theorem only evaluates them at one fixed multi-index.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin-4 indices are plugged into the fold definition of m2Num and the pattern-match table of explicitZ; the kernel checks integer equality and closes the goal. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,,N=8Z$ by exhausting Fin-4 cases. Each chunk theorem such as this one supplies one (or a block of) decided equalities that the assembler relies on to finish the universal statement.
In the broader Gravity/Regge strand of Recognition Science, the identity certifies that the midpoint M2 numerator is exactly eight times a sparse explicit kernel. That algebraic reduction is infrastructure for later continuum or continuum-limit comparisons; it is not itself a forcing-chain (T0–T8) step, but it hardens the discrete geometric side of the gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.