e_232131
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at index tuple (2,3,2,1,3,1) equals eight times the explicit integer table value. Gravity analysts cite it when assembling the full 4D midpoint M2 TT numerator identity. Proof is a single kernel `decide` on concrete Fin-4 data.
Claim. For indices $(a,b,c,d,i,j)=(2,3,2,1,3,1)$ in $\{0,1,2,3\}^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 11 of a 256-case kernel certifying that the folded 4D Regge midpoint numerator equals eight times a closed-form integer table. The ambient setting is the exact midpoint M2 TT identity in discrete gravity analysis.
The numerator m2Num is defined by folding a fixed coupling list: it sums contribution terms contrib t a b c d i j over that list, yielding an integer for each six-tuple of Fin 4 indices. The companion table explicitZ is a pattern-matched integer function on the same six indices (sample clauses include values $4$, $-2$, and so on).
The local claim is one concrete instance of $m_2^{\mathrm{num}}=8Z$ inside that finite kernel.
proof idea
One-line computational proof: by decide. Both sides are closed integer expressions once the six Fin 4 arguments are fixed to $2,3,2,1,3,1$, so the kernel reduces the equality of two concrete Int values with no further lemmas.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one decided cell of that case tree.
In the Recognition gravity stack this closes a purely algebraic numerator identity used when matching discrete Regge midpoint curvature data to the continuum TT sector. It is bookkeeping, not a new physical law: the physics content sits in the parent identity and the surrounding Regge analysis, not in any single index tuple.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.