e_221012
plain-language theorem explainer
For the six-index slot (2,2,1,0,1,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=2$, $c=1$, $d=0$, $i=1$, $j=2$ in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit integer kernel: $\mathrm{m2Num}(2,2,1,0,1,2)=8\cdot\mathrm{explicitZ}(2,2,1,0,1,2)$.
background
In the Regge exact-midpoint 4D analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator m2Num folds a fixed coupling list, summing a local contribution at each triple against the six free indices. The companion explicitZ is a sparse case table of small integers (e.g. $\pm 2,4$) on selected index patterns and zero elsewhere.
The module is chunk 10 of a 256-way partition of the Fin-4^6 domain. Each chunk discharges one concrete equality m2Num = 8·explicitZ by kernel computation, so the global identity can be assembled by exhaustive fin_cases without re-running the fold at the top level.
Upstream, explicitZ and m2Num are pure definitions in the kernel certificate module; this theorem only evaluates them at one point.
proof idea
One-line proof by decide. Lean reduces both sides at the concrete Fin-4 sextuple (2,2,1,0,1,2): the left-hand fold over couplingZList and the right-hand 8·explicitZ lookup become closed integer literals, and decidable equality on Int closes the goal. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,;\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ by six nested fin_cases. That global identity is the algebraic backbone of the Regge midpoint M2 TT identity in 4D gravity analysis inside the monolith.
Within Recognition Science gravity work, certifying the numerator against the explicit kernel keeps the discrete curvature bookkeeping exact rather than approximate. The chunking pattern (256 decides) is pure computational hygiene: each point equality is tiny and machine-checkable, while the parent theorem packages them into the quantified claim downstream consumers need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.