e_210010
plain-language theorem explainer
For the six-index tuple (2,1,0,0,1,0) in (Fin 4)^6, the folded numerator m2Num equals eight times the closed-form explicitZ value. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,\,b{=}1,\,c{=}0,\,d{=}0,\,i{=}1,\,j{=}0$ in $\mathbb{F}_4$, the coupling-fold numerator satisfies $m_2^{\mathrm{num}}(2,1,0,0,1,0)=8\,Z_{\mathrm{expl}}(2,1,0,0,1,0)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator m2Num is the fold of a fixed coupling list: it sums a local contribution over every coupling term. The comparison target explicitZ is a sparse closed form, nonzero only on a short list of index patterns (e.g. value 4 on (0,0,1,1,2,2), value −2 on several mixed pairs).
The module is chunk 9 of a 256-cell partition of the full (Fin 4)^6 table. Each cell asserts the scalar identity numerator = 8 · explicit form at one concrete multi-index. The factor 8 is the global normalization that makes the two kernels match everywhere.
Upstream definitions live in the KernelCert module: m2Num is pure accumulation; explicitZ is pattern-matched Int data. No analytic continuum input enters these cells.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are fixed: the fold in m2Num evaluates over the finite coupling list, and explicitZ matches a single pattern (or defaults). Lean’s kernel decision procedure checks integer equality; no lemmas are invoked.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in (Fin 4)^6. Its proof is nested fin_cases on all six indices; each leaf discharges via one of these chunk cells (siblings e_210000 … e_210023 and the other chunks).
In the Recognition gravity stack this closes the discrete algebraic step of the Regge midpoint M2–TT identity in 4D: once numerator and explicit kernels agree pointwise, continuum or continuum-limit arguments can treat them as interchangeable. It is pure finite combinatorics, not a continuum curvature claim, and does not itself invoke the forcing chain (T0–T8) or the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.