e_113012
plain-language theorem explainer
At multi-index (1,1,3,0,1,2) on (Fin 4)^6, the folded numerator coupling equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one atomic kernel cell in the Regge midpoint m2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,1,3,0,1,2)$ with each coordinate in $\mathbb{F}_4$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 5 of a 256-cell kernel certification that the Regge-exact midpoint numerator coupling agrees with an explicit integer table, scaled by eight. The ambient setting is 4D discrete gravity analysis: six indices each run over Fin 4, and equalities are decided by pure integer arithmetic.
The numerator side $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at the six indices. The comparison table $Z$ is an explicit case-split function Fin 4^6 → ℤ (sample clauses include values 4, −2, and so on). The claim under audit is one concrete cell of that comparison.
Upstream, both sides are pure definitions in the kernel certificate module; no analytic hypotheses are carried. Downstream assembly will quantify over all six indices by exhaustive fin_cases.
proof idea
One-line computational proof: decide evaluates both sides at the fixed six-tuple. The left side reduces by unfolding the fold over the coupling list; the right side multiplies the matched explicitZ clause by 8. No lemmas beyond kernel evaluation are required.
why it matters
Parent theorem m2Num_eq_eight_explicitZ asserts the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by nested fin_cases; each leaf is one of these chunk theorems. This declaration discharges the single cell (1,1,3,0,1,2).
In the gravity analysis stack, the identity certifies that the midpoint Regge numerator matches a sparse explicit integer kernel (scaled by eight), which is the algebraic backbone for later continuum or continuum-limit comparisons. It is bookkeeping inside the 4D kernel, not a forcing-chain landmark (T5–T8), but it is load-bearing for any claim that quotes the closed-form Z table in place of the folded coupling sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.