e_131030
plain-language theorem explainer
For the six-tuple of indices (1,3,1,0,3,0) in Fin 4, the Regge midpoint numerator equals eight times the explicit closed-form Z value at those indices. Gravity analysts assembling the full 4D M2–TT identity cite this as one of the 256 kernel cases. The proof is a single kernel decision (`decide`).
Claim. For indices $(a,b,c,d,i,j)=(1,3,1,0,3,0)$ with each entry in $\mathbb{F}_4$, the midpoint numerator $m_2^{\mathrm{num}}(1,3,1,0,3,0)$ equals $8$ times the explicit integer $Z(1,3,1,0,3,0)$.
background
In the 4D Regge exact-midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a coupling list: each term contributes an integer contrib at a six-index slot in $(\mathrm{Fin},4)^6$, and the fold starts from zero. The companion map $Z_{\mathrm{explicit}}$ is a sparse case table on the same six indices, returning small integers such as $4$, $-2$, and so on.
The module is chunk 7 of a 256-case kernel certification that $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$ pointwise. The local setting is pure finite enumeration over $\mathrm{Fin},4$, not continuum GR: every identity is an equality of integers computed from the coupling fold versus the explicit table.
proof idea
One-line computational proof: decide asks the kernel to evaluate both sides at the concrete indices $(1,3,1,0,3,0)$ and confirm integer equality. No lemmas are invoked beyond the definitions of the numerator fold and the explicit $Z$ table; the values are closed under reduction.
why it matters
This case is one brick in the exhaustive proof of $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$ for all six-tuples, the parent theorem in the assemble module. That universal identity is the algebraic core of the Regge exact-midpoint M2–TT certificate in 4D gravity analysis inside the Recognition Science monolith.
Downstream, the assemble theorem introduces six $\mathrm{Fin},4$ variables and runs nested fin_cases, discharging each concrete goal by a chunk equality of this form. The factor of eight links the folded coupling numerator to the sparse explicit table, keeping the 4D discrete curvature bookkeeping exact rather than approximate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.