e_301203
plain-language theorem explainer
Pointwise identity: the folded M2 numerator at index sextuple (3,0,1,2,0,3) equals eight times the explicit kernel table entry at those same indices. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite it as one kernel cell. The proof is a single native `decide` on concrete integers.
Claim. For the index sextuple $(3,0,1,2,0,3)\in(\mathbb{F}_4)^6$, the folded integer numerator $m_2^{\mathrm{num}}(3,0,1,2,0,3)$ equals $8$ times the explicit kernel value $Z(3,0,1,2,0,3)$.
background
This module sits in the 4D Regge exact-midpoint analysis of the M2–TT identity. The local goal, stated in the module header, is to certify $m_2^{\mathrm{num}}=8\cdot Z$ on one chunk of the $4^6$ index space by kernel decides.
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 $\mathbb{F}_4$ indices. The comparison target $Z$ is an explicit integer-valued table on $(\mathbb{F}_4)^6$, given by pattern-matching clauses (for example $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both definitions live in the kernel certificate module imported here. The present declaration fixes one concrete sextuple and asserts the scalar relation at that cell.
proof idea
One-line computational proof: decide. After the six indices are substituted, both sides reduce to closed integer expressions (a finite fold versus a table lookup), and Lean’s decision procedure checks equality of the resulting Int values. No lemmas beyond the two defining defs are invoked.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states the universal claim $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ on all of $(\mathbb{F}_4)^6$. Its proof case-splits every coordinate; each leaf is a cell identity of this form. Chunk 12 supplies one block of those leaves.
In the broader gravity stack this identity is bookkeeping for the exact midpoint M2–TT kernel in four dimensions: once every cell matches, the folded numerator may be replaced by the closed table $Z$, simplifying later curvature and coupling arguments. It does not itself touch the forcing chain (T0–T8), $\varphi$, or the eight-tick octave; it is pure discrete-kernel algebra inside the Regge analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.