e_120212
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (1,2,0,2,1,2) equals eight times the explicit integer kernel at that same index. Gravity analysts cite it as one cell in the 4D Regge midpoint M2 TT numerator certification. The proof is a single kernel `decide` on two closed integer expressions.
Claim. For indices $(a,b,c,d,i,j)=(1,2,0,2,1,2)$ in $(\mathrm{Fin}\,4)^6$, the folded 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 sits in the 4D Regge midpoint analysis of the M2 TT identity. The local goal, stated in the module header, is to certify $m_2^{\mathrm{num}}=8\cdot Z$ on one chunk of the finite index space by kernel decision (256 decides per chunk).
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 entry at the six $\mathrm{Fin},4$ indices. The comparison target $Z$ is an explicitly tabulated integer function on $(\mathrm{Fin},4)^6$, with sparse nonzero values such as $4$ on diagonal-type slots and $-2$ on selected off-diagonal patterns.
The full universal statement ranges over all $4^6$ sextuples. That quantification is assembled elsewhere by exhaustive fin_cases; the present file only discharges one concrete cell of that grid.
proof idea
One-line kernel proof: decide. Both sides are closed Int terms once the six concrete Fin 4 numerals are substituted into the fold definition of the numerator and the pattern-match definition of $Z$. Lean reduces the equality in the kernel with no lemmas and no arithmetic rewriting beyond evaluation.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and proves it by six nested fin_cases over $\mathrm{Fin},4$. Each chunk theorem such as this one supplies a decided cell so the universal identity is not a single monolithic kernel goal.
In the Recognition gravity stack, the certified numerator identity is part of the exact midpoint M2 TT bookkeeping in 4D Regge calculus. It is computational scaffolding rather than a forcing-chain landmark (T5–T8), but it locks the discrete curvature/coupling algebra that later continuum or continuum-limit arguments rely on. No open physics claim is settled here; only one index cell of the algebraic identity is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.