e_023203
plain-language theorem explainer
Pointwise identity: the folded midpoint numerator at multi-index (0,2,3,2,0,3) equals eight times the explicit integer kernel table at that same index. Gravity analysts proving the global Regge exact midpoint M2TT numerator identity cite this chunk among the 256 kernel decides. The proof is a single computational `decide` on concrete integers.
Claim. For the multi-index $(0,2,3,2,0,3)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit kernel table entry: $m_2^{\mathrm{num}}(0,2,3,2,0,3)=8\,Z_{\mathrm{expl}}(0,2,3,2,0,3)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin 4 indices are compared. The numerator m2Num is defined by folding a fixed coupling list: it sums a local contribution at each coupling triple for the given index sextuple. The companion explicitZ is a closed pattern-match table returning a small integer (typical values 4, -2, and so on) for each sextuple.
The module is chunk 2 of a 256-way split of the kernel: each chunk theorem asserts the scalar identity numerator = 8 · table at one concrete multi-index. The factor eight is the global normalization relating the folded sum to the explicit table across the whole kernel.
Upstream, only the two definitions are needed; no analytic lemma is required because both sides evaluate to concrete Int values once the indices are fixed.
proof idea
One-line computational proof: by decide. Both sides are closed integer expressions once the six Fin 4 arguments are literals, so the kernel decision procedure discharges equality without lemmas or rewriting.
why it matters
This is one atomic cell in the proof that the folded midpoint numerator equals eight times the explicit kernel everywhere. The parent theorem m2Num_eq_eight_explicitZ introduces six free Fin 4 variables and runs nested fin_cases, each leaf landing on a chunk identity of this form. Without the full set of 256 decides, the global numerator identity (and thus the Regge exact-midpoint M2TT certificate that depends on it) does not close.
In the broader gravity stack this is pure kernel bookkeeping: it does not itself invoke Recognition landmarks (T5–T8, RCL, phi-ladder), but it is load-bearing scaffolding for the discrete curvature / midpoint identities those landmarks eventually constrain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.