e_230232
plain-language theorem explainer
For the six Fin-4 multi-index (2,3,0,2,3,2), the folded numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of the 256 kernel cells. The proof is a pure decide on integer arithmetic.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,3,0,2,3,2)$ with each entry in $\{0,1,2,3\}$, the folded coupling numerator $N_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $N_2$ (Lean m2Num) is defined by folding a fixed coupling list: it sums a local contribution over every coupling triple. The closed form $Z$ (Lean explicitZ) is a sparse pattern-match table of small integers (entries such as $4$, $-2$, and so on).
The module is chunk 11 of a 256-cell kernel certification: the claim is the pointwise identity $N_2=8Z$ on the full $4^6$ grid. Upstream, only the two definitions are needed; no analytic lemma is imported. Downstream assembly will reassemble all cells into a single quantified statement.
proof idea
One-line computational proof: decide evaluates both sides as concrete Int expressions. The left-hand side runs the fold that defines m2Num at the fixed indices $(2,3,0,2,3,2)$; the right-hand side looks up explicitZ at the same indices and multiplies by eight. Equality of the resulting integers is decided by the kernel.
why it matters
This cell is one brick in the exhaustive proof that $N_2=8Z$ everywhere on Fin-4^6. The parent theorem m2Num_eq_eight_explicitZ quantifies over all six indices and discharges the grid by fin_cases, invoking each chunk identity (including this one) as a leaf. That global identity is the algebraic core of the Regge exact midpoint M2–TT certificate in 4D gravity analysis inside the Recognition stack. It does not itself touch the forcing chain (T0–T8) or the J-cost; it sits downstream in the discrete-gravity layer that must match continuum TT structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.