e_200121
plain-language theorem explainer
For the six-index slot (2,0,0,1,2,1) on Fin 4, the folded numerator coupling m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts cite it as one atomic cell in the 4D Regge midpoint M2–TT identity certification. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,0,1,2,1)$ in $\mathrm{Fin}\,4$, the folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge-exact midpoint certification that the numerator coupling equals eight times an explicit integer table. The ambient setting is discrete gravity on a 4-simplex lattice: couplings are assembled by folding a fixed contribution list over six Fin-4 indices.
Upstream, m2Num is the fold of contrib over couplingZList, yielding an Int for each six-tuple. explicitZ is the closed-form lookup table on the same domain (sample entries include $4$, $-2$, and so on for distinguished index patterns). The module header states the local goal: prove $m_2^{\mathrm{num}}=8\cdot Z$ by 256 kernel decides, of which this declaration is cell 8 of its block.
Sibling theorems cover the neighboring index patterns in the same chunk; together they feed a universal quantifier over all $4^6$ slots.
proof idea
One-line computational discharge: by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted into the fold definition of m2Num and the pattern-match definition of explicitZ; the kernel checks equality of those integers. No lemmas are invoked beyond the definitions themselves.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts the identity for every six-tuple by exhaustive fin_cases on each coordinate; each case lands on a chunk theorem such as this one. Without the per-cell equalities, the assemble step cannot close.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint evaluation of the M2–TT sector in 4D Regge calculus. It does not itself invoke the forcing chain (T5–T8) or the J-cost, but it sits inside the discrete-gravity layer that must match continuum limits once the eight-tick and $D=3$ structure are in place. Closing all chunks removes a scaffolding gap in the 4D kernel certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.