e_333203
plain-language theorem explainer
For the single multi-index (3,3,3,2,0,3) on Fin 4, the folded numerator coupling m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2TT numerator identity. The proof is a pure kernel decision: Lean closes the integer equality by decide.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Write $N$ for the folded coupling numerator (sum of all list contributions at those indices) and $Z$ for the explicit integer kernel at the same indices. Then $N(3,3,3,2,0,3)=8\,Z(3,3,3,2,0,3)$.
background
This module sits in the 4D Regge-calculus analysis of the exact midpoint M2TT identity. The local goal, stated in the module header, is to certify the pointwise relation m2Num = 8·explicitZ on one chunk of the six-index kernel (chunk 15 among the 256 decide obligations).
The numerator m2Num(a,b,c,d,i,j) is defined by folding a fixed coupling list: start at 0 and add each contribution term at the six Fin-4 indices. The comparison target explicitZ is a closed-form integer table on (Fin 4)^6, with sparse nonzero entries such as 4 or -2 on selected index patterns.
Both definitions live in the KernelCert import. The present declaration fixes one concrete six-tuple and asserts the scalar identity at that point.
proof idea
One-line computational proof: by decide. After unfolding m2Num (the fold over couplingZList) and explicitZ at the concrete indices 3,3,3,2,0,3, both sides reduce to closed integers; the kernel decision procedure checks equality. No lemmas beyond the two definitions are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles the universal statement ∀(a b c d i j : Fin 4), m2Num = 8 * explicitZ by nested fin_cases on all six indices. Each leaf is one of these e_* decide theorems; this declaration is the leaf for (3,3,3,2,0,3).
In the broader Recognition gravity stack, the identity underwrites exact algebraic control of the midpoint Regge M2TT numerator in 4D, so curvature and mass-ladder comparisons can quote a fully expanded integer kernel rather than an opaque fold. It does not itself touch the T0–T8 forcing chain or the J-cost RCL; it is infrastructure inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.