e_012003
plain-language theorem explainer
For the single index sextuple (0,1,2,0,0,3) on Fin 4, the M2 numerator equals eight times the explicit closed-form integer Z. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite it as one kernel cell. The proof is a pure `decide` check on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,2,0,0,3)$ in $(\mathrm{Fin}\,4)^6$, the M2 numerator $m_2^{\mathrm{num}}(0,1,2,0,0,3)$ equals $8\,Z(0,1,2,0,0,3)$, where $Z$ is the explicit integer table and $m_2^{\mathrm{num}}$ is the fold of coupling contributions.
background
The module sits in the 4D Regge midpoint analysis of the M2–TT identity. It is chunk 1 of a 256-cell kernel that discharges the pointwise equality between two integer-valued tensors on $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at those six indices. The comparison object $Z(a,b,c,d,i,j)$ is an explicit case table of small integers (entries such as $4$, $-2$, and so on) that is meant to be the closed form of that fold, up to the universal factor 8.
Local goal of the chunk: verify $m_2^{\mathrm{num}}=8Z$ on one concrete sextuple so the assembler can cover all $4^6$ cells by finite case split.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values (the fold on the left, the matching table clause on the right), and the kernel checks equality. No lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases. That global equality is the algebraic core of the Regge-exact midpoint M2–TT identity in four dimensions: it certifies that the folded coupling numerator is exactly eight times the closed-form table, cell by cell.
In the Recognition gravity stack this is bookkeeping infrastructure rather than a forcing-chain landmark (T0–T8). It closes one of the 256 kernel obligations that make the 4D midpoint identity fully computational and sorry-free. Downstream geometry and continuum-limit arguments can then quote the assembled identity without re-checking individual index cells.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.