e_010231
plain-language theorem explainer
At multi-index (0,1,0,2,3,1) the folded 4D Regge midpoint numerator m2Num equals eight times the explicit integer table explicitZ. Gravity analysts cite it as one atomic kernel check inside the full m2Num = 8·explicitZ identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,2,3,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit closed-form integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on every 6-tuple of $\mathrm{Fin},4$ indices in the 4D Regge exact-midpoint TT identity kernel.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The companion $Z$ is an explicit pattern-matched integer table on the same six indices (sample clauses send $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local claim is only the single point $(0,1,0,2,3,1)$; siblings cover the rest of the chunk.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values (the fold of m2Num at fixed indices versus 8 times the matching explicitZ clause), so the equality is a decidable integer identity with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges the universal quantifier by exhaustive fin_cases on all six indices. Each atomic e_* fact (this one included) is one leaf of that case tree.
In the Recognition gravity stack this closes the numerator side of the 4D Regge exact-midpoint mass-squared TT identity, converting a folded coupling sum into a sparse explicit integer table. It is pure discrete linear algebra on $\mathrm{Fin},4$; it does not itself invoke the T0–T8 forcing chain, $\phi$-ladder masses, or the RCL, but it is infrastructure those continuum limits sit on once the kernel is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.