e_001031
plain-language theorem explainer
For the multi-index sextuple (0,0,1,0,3,1) on Fin 4, the folded coupling numerator m2Num equals eight times the explicit integer table entry explicitZ. Gravity analysts cite it as one atomic cell in the 256-case kernel that certifies the Regge midpoint M2 numerator identity in 4D. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0,b{=}0,c{=}1,d{=}0,i{=}3,j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the corresponding explicit integer table value: $\mathrm{num}(0,0,1,0,3,1)=8\cdot Z(0,0,1,0,3,1)$.
background
The ambient module is a chunk of the 4D Regge exact-midpoint M2/TT identity certification. The numerator side is the integer-valued map obtained by folding a fixed coupling list: each term contributes an integer depending on a sextuple of Fin-4 indices, and the fold starts from 0. Parallel to that fold sits an explicit closed-form table Z on the same index domain, returning small integers (typically $\pm 2,\pm 4$, or 0 on unlisted patterns).
The local claim of the chunk is the pointwise identity numerator $= 8\cdot Z$ on a block of the $4^6=4096$ index space; this file handles chunk 0 via 256 kernel decides. Upstream, both the fold definition and the table are supplied by the kernel-cert module; neither carries a proof, only the raw data the decides evaluate.
proof idea
One-line computational proof: by decide. Lean reduces both sides on the concrete Fin-4 sextuple $(0,0,1,0,3,1)$ to bare integers (the fold over the coupling list versus eight times the table lookup) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
This cell is consumed by the assembly theorem that states the identity for every sextuple: after introducing the six Fin-4 variables it runs nested fin_cases, and each concrete branch lands on a decide of this form. Closing all branches yields the global equality between the folded M2 numerator and eight times the explicit Z table, which is the algebraic core of the Regge exact-midpoint M2/TT identity in 4D.
Within Recognition gravity analysis the identity is bookkeeping infrastructure rather than a forcing-chain step (T0–T8); it certifies that the discrete curvature/numerator side matches the closed table used downstream in continuum or continuum-limit arguments. It does not itself touch $\phi$, the eight-tick octave, or the $\alpha$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.