e_310313
plain-language theorem explainer
At multi-index (3,1,0,3,1,3) the folded numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite this as one of the 256 pointwise kernel checks that assemble into the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete Fin-4 integers.
Claim. For the multi-index $(3,1,0,3,1,3)\in(\mathbb{F}_4)^6$, the integer numerator $m_2^{\mathrm{num}}(3,1,0,3,1,3)$ equals $8$ times the explicit kernel value $Z(3,1,0,3,1,3)$.
background
In the 4D Regge midpoint analysis the numerator m2Num is defined by folding a fixed coupling list: it sums contrib terms over couplingZList at a six-tuple of Fin-4 indices. The companion explicitZ is a sparse case table on those same indices, returning small integers such as 4, -2, or 0 on the support of the kernel.
The local module is chunk 13 of a 256-way partition of the Fin-4^6 domain. Each chunk discharges one concrete equality m2Num a b c d i j = 8 · explicitZ a b c d i j by kernel decision, so the later assembly theorem can reassemble the universal identity by fin_cases.
Upstream, explicitZ and m2Num live in the KernelCert module; this chunk only evaluates them at the fixed point (3,1,0,3,1,3).
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values (m2Num by folding the coupling list; explicitZ by its match table), and the kernel decision procedure checks the equality m2Num 3 1 0 3 1 3 = 8 * explicitZ 3 1 0 3 1 3 with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states ∀ (a b c d i j : Fin 4), m2Num a b c d i j = 8 * explicitZ a b c d i j and is proved by exhaustive fin_cases, each case landing on a chunk such as this one. That global identity is the algebraic backbone of the Regge exact midpoint M2 TT identity in 4D gravity analysis inside Recognition Science: it certifies that the folded numerator is exactly eight times the closed-form kernel on the entire discrete index space. Without the pointwise chunks the assembly cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.