e_033211
plain-language theorem explainer
For the six-index tuple (0,3,3,2,1,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form explicitZ value. Gravity analysts cite it as one atomic case in the exhaustive 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,2,1,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(0,3,3,2,1,1)=8\,Z_{\mathrm{explicit}}(0,3,3,2,1,1)$.
background
The module is one chunk of the 4D Regge-exact midpoint identity for the M2–TT sector: the claim that the folded numerator equals eight times a sparse explicit integer table, discharged by 256 kernel decides.
Upstream, m2Num is the fold of contrib over couplingZList at six Fin-4 indices, returning an Int. explicitZ is the matching closed-form table (nonzero only on a short list of index patterns, e.g. 4 or -2). Both live in the kernel-cert module imported here.
Local setting is pure finite enumeration: every sextuple in $(\mathrm{Fin},4)^6$ is a separate decide lemma; this file owns chunk 3.
proof idea
One-line by decide. Lean reduces both sides at the concrete indices (0,3,3,2,1,1) to integers and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 indices and proves it by nested fin_cases, dispatching each leaf to a chunk lemma of this form. Closing every leaf certifies that the folded Regge midpoint numerator is exactly eight times the explicit Z table in 4D, a computational step in the gravity-analysis chain toward the exact midpoint M2–TT identity. Not itself a forcing-chain (T0–T8) step; it is infrastructure under the discrete gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.