e_033113
plain-language theorem explainer
For the six-index slot (0,3,3,1,1,3) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it when assembling the full pointwise identity m2Num = 8·explicitZ over the 4D midpoint Regge kernel. The proof is a single kernel decide on that concrete integer equality.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,1,1,3)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(0,3,3,1,1,3)=8\,Z_{\mathrm{explicit}}(0,3,3,1,1,3)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices appear. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing local contributions at $(a,b,c,d,i,j)$. The companion $Z_{\mathrm{explicit}}$ is a sparse case table of small integers (entries such as $4$, $-2$, and defaults) that packages the closed-form kernel.
The module is chunk 3 of a 256-way split of the kernel certification: each chunk discharges a block of concrete index tuples so that the global identity can be reassembled by exhaustive fin_cases. Local setting: prove $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$ pointwise by decidable integer arithmetic, without symbolic simplification of the fold.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are fixed: the left via the fold definition of m2Num over couplingZList, the right via the pattern-match table for explicitZ scaled by 8. The kernel checks equality of those integers; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and proves it by nested fin_cases over Fin 4. Each chunk theorem such as this one supplies one residual goal in that case tree. The identity is infrastructure for the exact midpoint M2 TT relation in the 4D Regge gravity analysis: once numerator and explicit kernel match everywhere, downstream curvature and stress-tensor identities can quote a single closed form rather than the fold. No Recognition forcing-chain landmark (T5–T8, RCL, phi) is touched directly; the result is pure discrete-kernel bookkeeping inside the gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.