e_020101
plain-language theorem explainer
For the Fin-4 index sextuple (0,2,0,1,0,1), the Regge midpoint numerator m2Num equals eight times the explicit Z-table entry. Gravity analysts cite it as one cell of the 4D kernel identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,1,0,1)$ in $(\mathrm{Fin}\,4)^6$, the midpoint numerator $m_2^{\mathrm{num}}(0,2,0,1,0,1)$ equals $8\,Z_{\mathrm{explicit}}(0,2,0,1,0,1)$, where $m_2^{\mathrm{num}}$ is the fold of coupling contributions and $Z_{\mathrm{explicit}}$ is the tabulated integer kernel.
background
This module is chunk 2 of a 256-cell kernel certification that the 4D Regge midpoint numerator agrees with eight times an explicit integer table. Indices run over Fin 4, i.e. the four discrete directions of a 4-simplex edge labeling.
Upstream, m2Num a b c d i j is defined by folding contrib over couplingZList, accumulating an Int. The companion explicitZ is a pattern-matched table on six Fin 4 arguments (sample clauses give values such as 4, -2, ...). The claim under audit is one concrete evaluation of the identity m2Num = 8 · explicitZ.
Local setting (module doc): certify m2Num = 8·explicitZ by exhaustive kernel decides, split into chunks so each file stays small.
proof idea
One-line proof: by decide. Both sides reduce to closed integer expressions once the six indices are literals, so Lean’s decision procedure compares the folded m2Num value against 8 * explicitZ at (0,2,0,1,0,1) with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all six Fin 4 arguments by nested fin_cases and discharges each cell via a chunk lemma of this form. That global equality is the algebraic core of the Regge exact-midpoint M2 TT identity in 4D: the numerator built from coupling contributions matches eight times the closed-form Z kernel. Within Recognition gravity analysis this is bookkeeping infrastructure, not a forcing-chain step (T0–T8), but it locks the discrete curvature kernel used downstream in 4D midpoint identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.