e_230010
plain-language theorem explainer
For multi-index (2,3,0,0,1,0), the folded Regge numerator equals eight times the tabulated explicit integer kernel. Gravity analysts certifying the 4D midpoint M2TT identity cite this as one exhaustive kernel cell. Proof is a single kernel `decide` on two concrete Int values.
Claim. At indices $(2,3,0,0,1,0)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer table entry: $m_2^{\mathrm{num}}(2,3,0,0,1,0)=8\,Z(2,3,0,0,1,0)$.
background
In the 4D Regge exact-midpoint M2TT analysis, two integer kernels on six Fin 4 indices are compared. The numerator folds a fixed coupling list, summing a per-coupling contribution at the given indices. The companion table is a sparse case map sending those indices to small integers (typical values 4, -2, and so on).
This module is chunk 11 of a 256-cell kernel certification that the folded numerator equals eight times the table pointwise. The local setting is pure discrete integer arithmetic: no continuum limit, no units, only exact Int equality on a finite index set.
proof idea
One-line kernel decision. Both sides of the claimed equality are closed Int terms at the fixed sextuple $(2,3,0,0,1,0)$. The tactic decide evaluates them and checks equality; no lemmas, rewrites, or case splits appear in the body.
why it matters
This cell is consumed by the assembly theorem that states the identity for every sextuple in $(\mathrm{Fin},4)^6$, proved by nested fin_cases on the six indices. That universal equality is the algebraic backbone of the Regge exact-midpoint M2TT certification in 4D gravity. Within the Recognition gravity stack, such exact discrete identities underwrite curvature bookkeeping without floating-point residue. The chunk split keeps each kernel decide small and independently checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.