e_200003
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,0,0,0,0,3) equals eight times the explicit Z-table entry there. Gravity analysts cite it as one cell of the 256-case kernel that underwrites the global m2Num = 8·explicitZ identity. Proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,0,0,0,3)$ 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
In the 4D Regge exact-midpoint analysis, two integer kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each multi-index. The comparison target is an explicit sparse integer table $Z$ on the same index set (nonzero only on a short list of patterns such as $(0,0,1,1,2,2)\mapsto 4$).
This module is chunk 8 of the 256 kernel decides that discharge $m_2^{\mathrm{num}}=8Z$ pointwise. The local setting is pure finite enumeration: every index runs in ${0,1,2,3}$, so each cell is a closed integer identity.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values at the fixed tuple $(2,0,0,0,0,3)$: the left via the fold definition of the numerator, the right via the pattern-match table for $Z$ (scaled by 8). The kernel checks equality of those integers; no lemmas beyond the two definitions are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and is proved by exhaustive fin_cases on the six indices. Each chunk lemma such as this one is a named cell in that 256-case grid.
In the broader gravity stack, the identity certifies that the midpoint Regge mass-squared numerator is exactly eight copies of the explicit $Z$ kernel, a bookkeeping step toward the 4D TT midpoint identities used in the Recognition gravity analysis. It is computational scaffolding, not a forcing-chain (T0–T8) step, but it closes a finite certificate the assembly theorem depends on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.