e_032011
plain-language theorem explainer
For the six-index slot (0,3,2,0,1,1) on Fin 4, the folded numerator coupling equals eight times the tabulated explicit kernel entry. Gravity analysts cite it when assembling the full pointwise identity m2Num = 8·explicitZ over the 4D midpoint Regge kernel. The proof is a single kernel decision (decide) on concrete integers.
Claim. At multi-index $(a,b,c,d,i,j)=(0,3,2,0,1,1)$ with each index in $\{0,1,2,3\}$, the folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 3 of a 256-case kernel certification that the 4D midpoint Regge numerator matches eight times a closed-form table. Indices run in $\mathrm{Fin},4$, i.e. the discrete 4-label set used for the exact midpoint M2TT identity.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the six indices. The comparison target $\mathrm{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern table (sample entries include $4$, $-2$, and so on for the listed index patterns).
Local goal of the chunk: discharge one concrete six-tuple so the assembler can glue all tuples into a single universal equality.
proof idea
One-line proof by decide. Both sides reduce to closed integer expressions: the left-hand side evaluates the fold of contrib over couplingZList at the fixed indices $(0,3,2,0,1,1)$; the right-hand side is $8$ times the matching explicitZ clause. Lean’s kernel decision procedure checks the resulting integer equality; no lemmas beyond the two definitions are required.
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 exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each chunk entry such as this one supplies (or is the residual of) one case in that $4^6$ cover.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge calculus kernel in 4D: once numerator and explicit table agree pointwise, downstream curvature and mass-ladder comparisons can quote a single closed form rather than a fold. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is pure discrete kernel algebra supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.