e_021332
plain-language theorem explainer
For the multi-index (0,2,1,3,3,2) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it when assembling the full 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(0,2,1,3,3,2)$. Then the summed coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-case kernel certification that the 4D Regge midpoint numerator matches eight times a closed-form integer table. The ambient setting is discrete gravity analysis: edge and face couplings on a 4-simplex skeleton, with all free indices ranging over Fin 4.
The numerator $N$ is defined by folding a fixed coupling list and summing each term's contribution at the six indices. The explicit kernel $Z$ is a pattern-matched integer table on those same indices (typical values $\pm 2,\pm 4$, and sparse support). The local claim is one concrete sextuple in that table identity $N=8Z$.
Upstream, both $N$ and $Z$ live in the kernel-cert module; this chunk only evaluates them at fixed arguments.
proof idea
One-line computational proof: decide reduces both sides to concrete Int values (the fold for the numerator and the match for the explicit kernel) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
The parent theorem m2Num_eq_eight_explicitZ exhausts all $4^6$ index sextuples by fin_cases and dispatches each cell to a chunk equality of this form. This declaration closes the cell $(0,2,1,3,3,2)$ inside chunk 2.
In the Recognition gravity stack, the identity $N=8Z$ is bookkeeping for the exact midpoint M2–TT comparison in 4D Regge calculus: once every cell matches, the assembled numerator is interchangeable with the explicit kernel, which is the form used in later curvature and continuum-limit arguments. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete-kernel certification supporting the gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.