e_213301
plain-language theorem explainer
For the six-index slot (2,1,3,3,0,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these micro-identities when assembling the global Regge midpoint M2TT equality. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2,b=1,c=3,d=3,i=0,j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
This module is chunk 9 of a 256-way case split proving that the Regge midpoint M2 numerator equals eight times a closed-form integer kernel on every 6-tuple of Fin 4 indices. The ambient setting is 4D discrete gravity analysis: couplings are summed, then matched to an explicit table.
The numerator m2Num is defined by folding contrib over couplingZList and accumulating an integer. The comparison target explicitZ is a pattern-matched table on six Fin 4 arguments (sample entries include 4, -2, and so on). Both live in the KernelCert module imported here.
Chunk theorems pin one concrete 6-tuple so the assembler can discharge the universal statement by exhaustive fin_cases.
proof idea
One-line tactic proof: decide. Both sides reduce to concrete integers once the six Fin 4 literals are substituted into the fold definition of the numerator and the pattern table for the explicit kernel; the kernel decision procedure checks equality.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for all six Fin 4 indices and proves it by nested fin_cases, invoking one chunk fact per cell. Without these micro-equalities the global Regge midpoint M2TT numerator identity cannot close.
In the Recognition gravity stack this is bookkeeping infrastructure for the discrete curvature/coupling side, not a forcing-chain landmark (T5–T8). It is pure certified arithmetic that lets later continuum or continuum-limit arguments trust the 4D midpoint kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.