e_220133
plain-language theorem explainer
For the six-index slot (2,2,0,1,3,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts certifying the 4D Regge exact-midpoint M2TT identity cite this as one atomic kernel cell. The proof is a single kernel decision equating both integer sides.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(2,2,0,1,3,3)$ equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(2,2,0,1,3,3)=8\,Z_{\mathrm{exp}}(2,2,0,1,3,3)$.
background
This module is chunk 10 of a 256-cell kernel certification that the 4D Regge exact-midpoint M2TT numerator equals eight times a closed-form integer table. Indices run over Fin 4 (four discrete directions).
m2Num a b c d i j is defined by folding couplingZList, accumulating each term's contrib at those six indices; the result is an Int. explicitZ is the matching closed-form table on the same six Fin 4 arguments (pattern-matched integer values such as 4, -2, and so on).
The local claim is one concrete cell of the identity m2Num = 8 · explicitZ. Upstream, both sides are pure definitions in the kernel-cert module; no analytic lemma is required beyond evaluating those definitions at fixed indices.
proof idea
One-line proof by decide. Lean reduces both m2Num 2 2 0 1 3 3 (the fold over couplingZList) and 8 * explicitZ 2 2 0 1 3 3 to concrete integers and checks equality in the kernel. No lemmas are invoked beyond definitional reduction.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the full universal statement $\forall a,b,c,d,i,j,; m2Num=8\cdot explicitZ$ by exhaustive fin_cases on all six Fin 4 indices. Each chunk cell such as this one discharges one branch of that case split.
In the Recognition gravity stack this kernel identity is bookkeeping for the exact-midpoint Regge M2TT analysis in 4D: it pins the discrete numerator against the explicit coupling table so later continuum or continuum-limit arguments can quote a fully certified algebraic identity rather than an unchecked expansion. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is infrastructure under the gravity-analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.