e_233302
plain-language theorem explainer
Pointwise identity: the summed coupling numerator at multi-index (2,3,3,3,0,2) equals eight times the explicit integer table entry. Gravity analysts assembling the 4D Regge midpoint M2TT numerator identity cite this kernel cell. The proof is a single kernel decision (`decide`) on concrete Fin-4 data.
Claim. For indices $(a,b,c,d,i,j)=(2,3,3,3,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer table value at that multi-index: $N(2,3,3,3,0,2)=8\,Z(2,3,3,3,0,2)$.
background
This module is chunk 11 of a 256-cell kernel certifying that the 4D Regge-exact midpoint M2TT numerator matches an explicit closed table, entry by entry. The ambient setting is discrete gravity analysis: curvature and coupling contributions on a 4-index combinatorial skeleton with midpoint evaluation.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list and summing each term's contribution at a six-tuple of $\mathrm{Fin},4$ indices. The comparison table $Z=\mathrm{explicitZ}$ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite pattern match (e.g. $(0,0,1,1,2,2)\mapsto 4$, off-diagonal sign patterns $\mapsto -2$, and so on).
The global claim is $N=8Z$ at every multi-index. Individual chunks discharge one concrete cell so the assembly theorem can recombine them without re-running the full fold in the parent proof.
proof idea
One-line computational certificate: by decide. Both sides are closed integer expressions once the six $\mathrm{Fin},4$ arguments are literals, so the kernel reduces the fold that defines the numerator and the match that defines the table, then checks integer equality. No lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ by exhausting $\mathrm{Fin},4$ on each slot. That universal identity is the algebraic backbone of the Regge-exact midpoint M2TT numerator analysis in four dimensions: it replaces a summed coupling expression by a sparse explicit integer table, scaled by eight.
Within Recognition Science gravity work, such exact discrete identities underwrite continuum limits and coupling normalizations on the combinatorial side of the forcing chain (spatial $D=3$ plus the discrete tick structure). This cell is bookkeeping, not a new physical law, but the parent equality is unusable until every kernel point is discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.