e_023101
plain-language theorem explainer
Pointwise kernel identity: the folded coupling numerator at multi-index (0,2,3,1,0,1) equals eight times the explicit integer table entry. Gravity analysts assembling the 4D Regge midpoint M2 TT identity cite these 256 chunk lemmas. The proof is a single computational decide on concrete Fin-4 integers.
Claim. For the multi-index $(0,2,3,1,0,1)\in(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(0,2,3,1,0,1)=8\,Z_{\mathrm{expl}}(0,2,3,1,0,1)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six indices in $\mathbb{F}4$ are compared. The folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the sum of local contributions over a fixed coupling list. The explicit table $Z{\mathrm{expl}}$ is a sparse case-split map sending selected sextuples to small integers (e.g. $\pm 2,4$) and the rest by the residual clauses of that definition.
The module is chunk 2 of a 256-way kernel certification that $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ at every point. Each chunk fixes one concrete sextuple so the equality becomes a closed integer computation.
proof idea
Both sides evaluate at the fixed indices $0,2,3,1,0,1$. Unfolding the fold that defines the numerator and the case table for the explicit kernel yields two concrete integers; decide discharges their equality. No algebraic lemma is invoked beyond definitional reduction.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for all six $\mathbb{F}_4$ indices by exhaustive fin_cases and invokes one chunk per cell. That global equality is the certified numerator half of the Regge-exact midpoint M2 TT identity in 4D gravity analysis inside the monolith. It is bookkeeping infrastructure, not a new physical law: once every chunk is in, the assembler closes without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.