e_313022
plain-language theorem explainer
Pointwise identity: the midpoint Regge m₂ numerator at multi-index (3,1,3,0,2,2) equals eight times the explicit Z-table entry. Gravity analysts cite it when assembling the universal 4D kernel identity m₂Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,0,2,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 table value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge midpoint $M_2$ TT-identity certification. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer weight at a six-index slot in $(\mathrm{Fin},4)^6$. The companion table $Z$ is an explicit case-split function on the same six indices, returning small integers (typically $\pm 2,\pm 4$, or $0$).
The local claim of the chunk family is the scalar relation $m_2^{\mathrm{num}}=8\cdot Z$ at every kernel point. With four values per index there are $4^6=4096$ slots; the work is partitioned into decide-chunks (here chunk 13) so each file stays inside the kernel's comfortable range.
Upstream, both $m_2^{\mathrm{num}}$ and $Z$ live in the kernel-cert module; this theorem only evaluates them at one concrete tuple.
proof idea
One-line computational proof: decide. Both sides reduce to closed integer expressions once the six Fin 4 arguments are literals, so the kernel compares the evaluated integers and closes the goal. No lemmas beyond the definitions of the numerator fold and the explicit $Z$ table are required.
why it matters
Feeds the assembled universal statement m2Num_eq_eight_explicitZ, which asserts $\forall(a,b,c,d,i,j),, m_2^{\mathrm{num}}=8\cdot Z$ by exhausting all Fin 4 cases. That identity is the algebraic core of the exact midpoint $M_2$ TT relation in the 4D Regge analysis: it converts a folded coupling sum into a sparse, human-auditable integer table.
In the broader Recognition gravity stack, certified discrete curvature identities underwrite continuum limits and the matching of geometric response to the forced $D=3$ spatial sector (T8) and the eight-tick causal structure (T7). This declaration is pure bookkeeping, but without the full 4096-point cover the assemble theorem cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.