e_302201
plain-language theorem explainer
Pointwise kernel identity: at multi-index (3,0,2,2,0,1) the folded coupling numerator equals eight times the explicit integer table. Gravity analysts cite it as one of 256 decides that assemble the 4D midpoint M2TT numerator identity. Proof is a single native decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,0,2,2,0,1)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(3,0,2,2,0,1)=8\,Z(3,0,2,2,0,1)$.
background
This module is chunk 12 of a 256-case kernel certification that the 4D Regge midpoint M2TT numerator matches an explicit integer table. Indices run over $\mathrm{Fin},4$ (four discrete directions).
The numerator $N=m2Num$ is defined by folding a fixed coupling list: start at 0 and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $Z=\mathrm{explicitZ}$ is a hand-written six-argument integer table (sample clauses: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and so on).
The local claim is the scalar equality $N=8Z$ at one concrete multi-index. Upstream definitions supply both sides; no analytic lemma is required beyond evaluating the fold and the table.
proof idea
One-line computational proof: decide. Both sides are closed integer terms once the six $\mathrm{Fin},4$ arguments are substituted, so the kernel reduces the equality to true by evaluation. No rewrite lemmas or induction.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,,N=8Z$ and discharges it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is a leaf of that case split (module doc: "m2Num = 8·explicitZ, chunk 12 (256 kernel decides)").
In the Recognition gravity stack this closes the algebraic identity between the folded Regge midpoint numerator and the explicit coupling table in 4D, a prerequisite for exact midpoint curvature bookkeeping. It does not itself invoke the T0–T8 forcing chain, but it sits inside the discrete geometric layer that later couples to continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.