e_112113
plain-language theorem explainer
For the six Fin-4 indices (1,1,2,1,1,3), the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel decides that assemble the exact midpoint M2TT identity in 4D Regge calculus. The proof is a single decide on integer equality.
Claim. With $a=b=i=1$, $c=2$, $d=1$, $j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel: $N(1,1,2,1,1,3)=8\,Z(1,1,2,1,1,3)$.
background
In the 4D Regge midpoint 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 tuple. The closed form explicitZ is a sparse pattern match returning small integers (typically $\pm 2$ or $4$) on selected index patterns and zero elsewhere.
The module is chunk 5 of a 256-way case split: each chunk discharges a block of concrete index sextuples by kernel decision. The local claim is the instance of m2Num = 8·explicitZ at (1,1,2,1,1,3).
Upstream, both m2Num and explicitZ live in the KernelCert module; the present file only evaluates them at fixed points.
proof idea
One-line tactic proof: decide. Lean reduces both sides to concrete integers (m2Num by folding the coupling list; explicitZ by pattern match) and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
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}$ and proves it by exhaustive fin_cases on the six indices. Each concrete e_* theorem is one leaf of that case tree.
In the Recognition gravity stack this identity certifies that the midpoint M2TT numerator is exactly eight times the sparse kernel, a bookkeeping step toward the exact 4D Regge midpoint formula. It is pure discrete algebra on Fin-4 indices, not a continuum GR claim, and does not itself invoke the forcing chain (T0–T8) or the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.