e_200202
plain-language theorem explainer
Concrete kernel equality: the midpoint Regge mass-squared numerator at multi-index (2,0,0,2,0,2) equals eight times the explicit Z-table entry. Gravity analysts cite it as one cell of the 256-point certificate that m2Num = 8·explicitZ on (Fin 4)^6. The proof is a single decide on fully evaluated integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,0,2,0,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 chunk 8 of a 256-cell kernel certificate for the 4D midpoint Regge identity $m_2^{\mathrm{num}}=8\cdot Z$. The ambient setting is discrete gravity analysis: a mass-squared numerator built from coupling data on a 4-index lattice, compared against a closed-form integer table.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a contribution function over couplingZList, summing integer terms at a fixed sextuple of Fin 4 indices. The comparison target explicitZ is a pattern-matched integer table on the same domain (sample clauses return $4$, $-2$, and similar small integers on distinguished index patterns).
The local claim is one pointwise instance of that table identity, with all six indices specialized to the concrete values $2,0,0,2,0,2$.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the fold for $m_2^{\mathrm{num}}$ and the pattern match for $Z$ are evaluated at the fixed indices, so the kernel decision procedure closes the equality with no lemmas or rewriting.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ and discharges the goal by exhaustive fin_cases on the six indices. Each chunk cell such as this one is a named, checkable witness that the folded numerator matches the explicit table at that lattice point.
In the broader gravity stack this is bookkeeping infrastructure for the exact midpoint $M_2$ TT identity in 4D Regge analysis, not a forcing-chain landmark (T5–T8) or an RCL step. It closes a finite certificate rather than an open analytic gap: once all 256 cells and the assembler are in place, the numerator/table relation is fully proved on the discrete index set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.