e_200310
plain-language theorem explainer
Pointwise kernel identity: the folded Regge numerator at multi-index (2,0,0,3,1,0) equals eight times the explicit integer table at that point. Gravity analysts cite it as one cell of the 4D midpoint M2 TT certification. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,0,3,1,0)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(2,0,0,3,1,0)=8\,Z_{\mathrm{expl}}(2,0,0,3,1,0)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathbb{F}4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $Z{\mathrm{expl}}$ is an explicit pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on).
This module is chunk 8 of a 256-cell decide grid that certifies $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ pointwise. The local setting is pure integer arithmetic on $\mathrm{Fin},4$ coordinates; no continuum limit or metric signature is invoked here.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple $(2,0,0,3,1,0)$. The left side reduces by unfolding the fold over couplingZList; the right side reduces by unfolding the pattern match for explicitZ. The resulting integer equality is discharged by the kernel decision procedure.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhaustive fin_cases. That global equality is the algebraic core of the Regge exact midpoint M2 TT identity certification in 4D gravity analysis inside the monolith.
Within Recognition Science this sits in the gravity layer that must match discrete curvature bookkeeping to continuum limits; it does not itself touch the T0–T8 forcing chain, but it hardens the discrete geometric substrate those continuum claims rest on. Closing all 256 chunks removes a scaffolding surface under the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.