e_032133
plain-language theorem explainer
Pointwise kernel identity: the folded M2 numerator coupling at multi-index (0,3,2,1,3,3) equals eight times the explicit Z-table entry at those indices. Gravity analysts cite it as one cell of the 4D Regge midpoint M2–TT numerator certification. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,2,1,3,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer table.
background
In the 4D Regge midpoint analysis, the M2–TT numerator is assembled from a finite list of coupling contributions. The function $m_2^{\mathrm{num}}$ folds that list, summing each contribution at a six-tuple of $\mathbb{F}_4$ indices. The companion table $Z$ is an explicit integer-valued function on the same index space, given by a finite case split (e.g. $(0,0,1,1,2,2)\mapsto 4$, mixed pairs $\mapsto -2$, and so on).
This module is chunk 3 of a 256-cell kernel certification that $m_2^{\mathrm{num}}=8Z$ holds at every index. The local setting is pure finite arithmetic over $\mathrm{Fin},4$, with no continuum limit or curvature hypothesis yet imposed.
proof idea
One-line kernel proof: decide evaluates both sides at the fixed indices $(0,3,2,1,3,3)$ and checks integer equality. The left side reduces by unfolding the fold over couplingZList; the right side multiplies the matching explicitZ clause by eight. No lemmas beyond the two definitions are required.
why it matters
Feeds the assembled theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhausting all $\mathrm{Fin},4$ cases. That global identity is the algebraic backbone of the exact midpoint M2–TT relation in the 4D Regge gravity analysis. Within Recognition Science gravity work, certifying the numerator table cell-by-cell keeps the discrete curvature bookkeeping machine-checked before continuum or phenomenological claims are attached. This cell is scaffolding closure for one of 256 kernel points, not a continuum theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.