e_213213
plain-language theorem explainer
Pointwise check that the midpoint M2 numerator equals eight times the explicit Z-table entry at discrete indices (2,1,3,2,1,3) in (Fin 4)^6. Gravity analysts assembling the 4D Regge TT-kernel identity cite it as one kernel cell. The proof is a single decide on integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(2,1,3,2,1,3)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge exact-midpoint analysis of the M2 TT identity. The numerator m2Num is defined by folding a fixed coupling list: it sums a local contribution at each coupling triple over the six Fin-4 indices. The companion table explicitZ is a closed integer pattern on those same six indices (sample clauses give values such as $4$ or $-2$ on diagonal and off-diagonal patterns).
The local setting is chunk 9 of a 256-cell decide kernel: each cell fixes one concrete hex-tuple and asserts the scalar identity numerator $= 8\cdot Z$. The factor eight is the global normalization relating the summed coupling form to the explicit table; this file only checks it pointwise.
Upstream, both sides are pure definitions in the kernel-cert module, so the equality is a finite integer computation once the indices are ground.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side evaluates the fold of contrib over couplingZList at the fixed indices $(2,1,3,2,1,3)$; the right-hand side looks up explicitZ at those indices and multiplies by 8. Lean’s kernel decision procedure discharges the resulting integer equality with no lemmas or case splits.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ and is proved by exhausting all six indices. That universal equality is the algebraic core of the 4D Regge exact-midpoint M2 TT-kernel certificate: it replaces a summed coupling expression by an explicit sparse integer table, making later curvature and graviton-mode identities computable by finite case analysis.
Within Recognition Science gravity work, this is bookkeeping infrastructure rather than a forcing-chain landmark (not T0–T8). It closes one cell of the decide kernel so the assembled identity can be cited without residual sorrys in the numerator layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.