e_301101
plain-language theorem explainer
For the multi-index sextuple (3,0,1,1,0,1) on Fin 4, the summed Regge coupling numerator equals eight times the explicit integer kernel entry. Gravity analysts cite it as one cell of the 4D midpoint M2–TT identity table. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=3$, $b=0$, $c=1$, $d=1$, $i=0$, $j=1$ in $\{0,1,2,3\}$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator $N$ is obtained by folding a fixed coupling list: each term contributes an integer depending on the six indices, and the fold starts at zero. The explicit kernel $Z$ is a closed case table of small integers (entries such as $4$, $-2$, and so on) on the same index domain.
The local module is chunk 12 of a 256-cell decide grid that checks $N=8Z$ pointwise. The surrounding certificate module defines both $N$ and $Z$; this file only discharges one concrete sextuple.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(3,0,1,1,0,1)$ and checks integer equality. No lemmas are invoked beyond the definitions of the numerator fold and the explicit kernel table.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 sextuple by nested fin_cases; each case lands on a chunk theorem of this form. Establishing $N=8Z$ everywhere is the algebraic core of the exact midpoint M2–TT identity in the 4D Regge gravity analysis. The identity is bookkeeping for discrete curvature couplings, not a continuum Einstein equation by itself, but it is required scaffolding before continuum or continuum-limit claims in this branch of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.