e_201323
plain-language theorem explainer
For the six-index slot (2,0,1,3,2,3) on Fin 4, the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over the 4D Regge midpoint kernel. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2,b=0,c=1,d=3,i=2,j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is one chunk of a 256-case kernel certification that the 4D Regge midpoint numerator equals eight times a closed-form integer table. The local setting is pure finite enumeration on $\mathrm{Fin},4$ indices: no continuum limit is taken here.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a contribution function at the six indices. The comparison object $\mathrm{explicitZ}$ is a pattern-matched integer table on those same six $\mathrm{Fin},4$ arguments (typical nonzero entries are $\pm 2$ or $4$).
The parent assembly theorem states the identity for every sextuple by exhaustive fin_cases; each chunk such as this one discharges one concrete sextuple so the assembly proof stays small.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold that defines $m_2^{\mathrm{num}}$ at $(2,0,1,3,2,3)$, the right-hand side multiplies the table value of $\mathrm{explicitZ}$ at the same indices by $8$. Lean’s kernel decision procedure checks the resulting integer equality.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z$ on $\mathrm{Fin},4$. That global identity is the algebraic backbone of the exact midpoint $M_2$ TT identity in the 4D Regge analysis used by the gravity sector of Recognition Science.
Without the chunked decides, the assembly proof would have to re-evaluate every fold in one place. Chunk 8 (this family) is one of the 256 kernel decides named in the module doc. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete bookkeeping that later continuum or continuum-limit gravity statements can trust.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.