e_210231
plain-language theorem explainer
For the six-index pattern (2,1,0,2,3,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these kernel-point equalities when assembling the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=1$, $c=0$, $d=2$, $i=3$, $j=1$ in $\mathrm{Fin}\,4$, the summed 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-point kernel certification that the Regge midpoint $M_2$ numerator agrees with an explicit closed form. The ambient setting is 4D discrete gravity analysis: six indices each run over $\mathrm{Fin},4$, and the claim is pointwise integer equality.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling triple at the six indices. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on those same six indices (typical values $\pm 2,,4$, and defaults elsewhere).
Chunk 9 packages many such pointwise facts so a later assembler can discharge the universal statement by exhaustive fin_cases rather than by a single giant decide.
proof idea
One-line proof by decide. Both sides are closed integer expressions once the six concrete Fin 4 arguments are substituted: the left side evaluates the fold that defines $m_2^{\mathrm{num}}$, the right side multiplies the table value of $\mathrm{explicitZ}$ by $8$. Lean’s kernel decision procedure checks the resulting integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by six nested fin_cases over $\mathrm{Fin},4$, each leaf a chunk equality of this form. That global identity is part of the Regge exact-midpoint $M_2$ TT certification in the gravity analysis stack: it replaces a summed coupling expansion by a sparse explicit kernel, which is what downstream curvature and continuum-limit arguments consume.
Within Recognition Science gravity work this is bookkeeping, not a forcing-chain step (T0–T8), but it is load-bearing for any claim that the discrete midpoint action matches the intended continuum kernel in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.