e_230303
plain-language theorem explainer
For the fixed multi-index (2,3,0,3,0,3) on Fin 4, the folded coupling numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts cite it as one cell of the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=3$, $c=0$, $d=3$, $i=0$, $j=3$ in $\{0,1,2,3\}$, the summed coupling numerator equals eight times the explicit integer kernel value at that sextuple: $N(2,3,0,3,0,3)=8\,Z(2,3,0,3,0,3)$.
background
This module is chunk 11 of a 256-cell kernel certification that the 4D Regge exact-midpoint M2TT numerator equals eight times a closed-form integer table. Indices run over Fin 4 (four discrete directions).
The numerator m2Num a b c d i j is defined by folding a fixed coupling list: start at 0 and add each term's contribution at the six indices. The comparison target explicitZ is a pattern-matched integer table on the same six Fin 4 arguments (sample entries include 4, -2, and further sparse values).
Local goal, per the module header: prove m2Num = 8 · explicitZ pointwise by decidable evaluation, one sextuple per lemma, then assemble.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel checks integer equality with no algebraic rewriting or named lemmas beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j : \mathrm{Fin},4,; N=8Z$ and is proved by exhaustive fin_cases on all six indices. Each chunk lemma such as this one discharges one concrete cell of that case split.
In the gravity analysis stack this certifies the exact midpoint M2TT identity in 4D Regge calculus: the folded coupling numerator matches the explicit kernel used downstream. It is pure discrete linear-algebra bookkeeping on the 4-direction index set, not a continuum GR derivation, and sits inside the broader Recognition gravity formalization rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.