e_230102
plain-language theorem explainer
One of 256 kernel cases for the 4D Regge midpoint identity: the M2 numerator at index tuple (2,3,0,1,0,2) equals eight times the explicit Z coupling at those same indices. Gravity analysts assembling the full pointwise identity cite this chunk. The proof is a single kernel `decide` on concrete integer arithmetic.
Claim. For the six indices $(a,b,c,d,i,j)=(2,3,0,1,0,2)$ in $\mathrm{Fin}\,4$, the folded M2 numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the M2 numerator is defined by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums contribution terms over that list. The companion map $\mathrm{explicitZ}$ is a sparse integer table on six $\mathrm{Fin},4$ indices (typical nonzero values $\pm 2,,4$).
The module is chunk 11 of a 256-case kernel certification that $m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$ pointwise. Each chunk discharges a block of concrete index sextuples so the assembler can recombine them by exhaustive fin_cases.
Upstream, both $m_2^{\mathrm{num}}$ and $\mathrm{explicitZ}$ live in the kernel certificate module; this theorem only evaluates them at one fixed sextuple.
proof idea
One-line kernel proof: by decide. Lean reduces both sides at the concrete indices $(2,3,0,1,0,2)$ to closed integers (via the fold definition of the numerator and the pattern-match table for explicit Z) and checks equality by decision procedure. No lemmas are invoked beyond definitional unfolding.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$ and proves it by six nested fin_cases over the 256 kernel decides. That global identity is the algebraic core of the Regge-exact midpoint M2/TT relation in 4D gravity analysis inside the monolith.
Within Recognition Science gravity work, these certified numerator identities underwrite discrete curvature bookkeeping on the eight-tick / $D=3$ lattice side; they do not themselves invoke the J-cost or phi-ladder, but they clear a computational bottleneck before continuum matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.