e_112231
plain-language theorem explainer
For the single multi-index (1,1,2,2,3,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts assembling the exact midpoint M2TT identity cite this as one atomic case among the 4^6 kernel checks. The proof is a pure kernel decide on two concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(1,1,2,2,3,1)=8\,Z_{\mathrm{explicit}}(1,1,2,2,3,1)$.
background
This module is chunk 5 of the exhaustive verification that the 4D Regge midpoint numerator equals eight times an explicit integer kernel. The ambient setting is discrete gravity analysis: couplings on Fin-4 multi-indices are summed into a numerator, then matched against a hand-written table.
m2Num a b c d i j folds couplingZList, accumulating each term's contrib at the six indices; the result is an Int. explicitZ is the matching closed-form table on Fin 4 → ⋯ → Fin 4 → Int, with sparse nonzero entries such as (0,0,1,1,2,2) ↦ 4 and sign-flipped off-diagonal patterns at -2.
The local claim is one sextuple inside that table identity. Downstream assembly will range over all six Fin 4 variables by fin_cases and invoke each chunk fact.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals, so the decidable equality on Int closes with no lemmas, rewrites, or case splits inside this declaration.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states the universal identity ∀ a b c d i j, m2Num a b c d i j = 8 * explicitZ a b c d i j and proves it by six nested fin_cases, each leaf landing on a chunk theorem of this form. Without the per-index decides, the assembly cannot discharge the 4^6 kernel.
In the Recognition gravity stack this is bookkeeping for the exact midpoint M2TT identity in 4D Regge calculus, not a new physical law. It sits under the broader program that discrete curvature and coupling numerators match closed forms before continuum or phenomenological limits are taken. No T0–T8 forcing step is proved here; the chunk only certifies one arithmetic cell of the gravity kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.