e_302202
plain-language theorem explainer
For the six-index tuple (3,0,2,2,0,2) on Fin 4, the folded Regge coupling numerator equals eight times the explicit integer kernel. Gravity analysts proving the 4D midpoint M2TT identity cite it as one finite case among the 256 kernel decides. The proof is a single computational `decide` on concrete integers.
Claim. For indices $a=3,b=0,c=2,d=2,i=0,j=2$ in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit kernel integer: $N(3,0,2,2,0,2)=8\,Z(3,0,2,2,0,2)$.
background
This module is chunk 12 of a 256-case kernel certification that the 4D Regge-exact midpoint numerator equals eight times an explicit integer table. Indices run over Fin 4 (four discrete directions).
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a local contribution at each term. The explicit kernel $Z$ is a pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on). The local claim is the pointwise identity $N=8Z$ at one concrete multi-index.
Upstream, both $N$ and $Z$ live in the kernel-cert module; this chunk only evaluates one slot.
proof idea
One-line computational proof: decide. After substituting the concrete Fin 4 arguments, both sides reduce to closed integer expressions (fold of contributions versus a table lookup times eight), and the decision procedure checks equality.
why it matters
Feeds the assembled theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and discharges the universal quantifier by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies a single case in that 256-fold split (module doc: "m2Num = 8·explicitZ, chunk 12").
In the Recognition gravity stack this identity is bookkeeping for the Regge-exact midpoint M2TT kernel in 4D: it replaces a summed coupling expression by a sparse explicit integer table, clearing algebraic noise before continuum or continuum-limit arguments. It does not itself invoke the T0–T8 forcing chain; it is infrastructure inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.