e_110313
plain-language theorem explainer
Pointwise identity: the folded midpoint numerator at Fin-4 indices (1,1,0,3,1,3) equals eight times the explicit integer kernel value. Gravity analysts cite it when assembling the full 4D Regge midpoint M2 TT identity. The proof is a single kernel `decide` on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,1,0,3,1,3)$ with each index in $\mathbb{F}_4$, the folded midpoint 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 chunk 5 of a 256-case kernel certification that the discrete midpoint numerator agrees with a closed-form table in 4D Regge analysis. Indices run over $\mathrm{Fin},4$, i.e. ${0,1,2,3}$.
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 object $\mathrm{explicitZ}$ is an integer-valued case table on the same six indices (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local claim is only the single sextuple $(1,1,0,3,1,3)$. Sibling theorems cover the other concrete points; the assembly theorem quantifies over all of $\mathrm{Fin},4^6$.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values (the fold for $m_2^{\mathrm{num}}$ at these indices, and eight times the matching explicitZ clause), so decidable integer equality closes the goal with no lemmas or rewriting.
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 discharges the universal goal by exhaustive fin_cases on the six $\mathrm{Fin},4$ arguments. Each concrete residue class is exactly one chunk identity of this form.
In the Recognition gravity stack this certifies that the midpoint M2 TT numerator matches its explicit kernel on the full 4D index set, a computational step toward the exact discrete curvature identities used in the Regge analysis layer. It does not itself invoke the forcing chain (T0–T8), RCL, or $\varphi$-ladder mass formulae; it is pure index algebra supporting those geometric claims upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.