e_233232
plain-language theorem explainer
For the six-index tuple (2,3,3,2,3,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel point-checks that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=3$, $c=3$, $d=2$, $i=3$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 11 of a 256-way case split proving that the Regge midpoint $M_2$ numerator equals eight times an explicit integer kernel on all six-tuples in $(\mathrm{Fin},4)^6$. The local setting is pure finite enumeration: no continuum limit, only integer arithmetic on discrete simplex labels.
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 $\mathrm{explicitZ}$ is a pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on for distinguished index patterns).
Upstream, both $m_2^{\mathrm{num}}$ and $\mathrm{explicitZ}$ live in the kernel certificate module. The present lemma fixes one concrete six-tuple and asserts equality after the factor of eight.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals: the fold that defines $m_2^{\mathrm{num}}$ evaluates, the pattern match that defines $\mathrm{explicitZ}$ evaluates, and Lean checks $n = 8\cdot z$ by kernel computation. No lemmas are invoked beyond the definitions of the two sides.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ by nested fin_cases over all six indices. Each chunk theorem such as this one discharges one residual goal in that case tree.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint $M_2$ TT kernel in 4D Regge calculus: once the numerator is replaced by the closed form $8Z$, later analytic steps can treat the kernel as an explicit integer table rather than a fold. It does not itself invoke the forcing chain (T0–T8) or the J-cost; it is infrastructure under the discrete gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.