e_232122
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,3,2,1,2,2) equals eight times the explicit integer table entry at that same index. Gravity analysts assembling the 4D Regge midpoint M2–TT kernel cite it as one of 256 concrete cells. The proof is a single kernel decide on fully evaluated integers.
Claim. For indices $(a,b,c,d,i,j)=(2,3,2,1,2,2)$ in $\mathbb{F}_4^6$, the folded 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 closed-form integer table on the same six indices.
background
In the 4D Regge exact-midpoint analysis, the M2–TT kernel numerator is defined by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums contrib terms over couplingZList. The companion table $Z$ (explicitZ) is a pattern-matched integer function on six Fin 4 indices, with sparse nonzero entries such as $4$ on diagonal-type patterns and $-2$ on selected off-diagonal patterns.
This module is chunk 11 of a 256-cell partition of the full kernel. The local goal, stated in the module header, is to certify $m_2^{\mathrm{num}}=8\cdot Z$ at each concrete sextuple by decision procedure, so a later assembler can quantify over all of $\mathbb{F}_4^6$.
proof idea
Both sides are closed integer expressions once the six Fin 4 arguments are fixed to $2,3,2,1,2,2$. The proof is the single tactic decide, which evaluates the fold defining the numerator and the pattern match defining the table, then checks equality of the resulting integers. No lemmas beyond the two definitions are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the universal quantifier by nested fin_cases, each leaf a chunk identity of this form. Without the pointwise cells, the assembler has nothing to case-split onto.
In the broader Recognition gravity stack, the identity is bookkeeping for the exact midpoint Regge kernel in four dimensions: it replaces a summed coupling expression by a sparse explicit table scaled by eight, which is the algebraic content needed before continuum or continuum-limit comparisons. It does not itself invoke the forcing chain (T0–T8) or the J-cost; it is pure discrete kernel arithmetic supporting those later gravity claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.