e_232201
plain-language theorem explainer
Concrete integer identity: the folded m2-numerator at Fin-4 indices (2,3,2,2,0,1) equals eight times the explicit Z-table entry there. Gravity analysts cite it as one cell of the 4D Regge midpoint TT kernel certification. The proof is a single kernel decide on closed arithmetic.
Claim. For the discrete index sextuple $(a,b,c,d,i,j)=(2,3,2,2,0,1)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(2,3,2,2,0,1)$ equals $8\,Z(2,3,2,2,0,1)$, where $Z$ is the explicit integer kernel table.
background
This module sits in the 4D Regge-exact midpoint analysis for the transverse-traceless (TT) gravity kernel. The local goal, stated in the module header, is to certify $m_2^{\mathrm{num}}=8\cdot Z$ on a 256-case chunk of the $4^6$ index space by kernel decision.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it sums a contribution functional over that list and returns an integer. The comparison table $Z$ is an explicit six-argument function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by pattern-matched constants (e.g. $4$, $-2$, and further cases).
Both objects live in the kernel-cert module imported here. The present declaration fixes one concrete sextuple inside chunk 11 and asserts the scalar identity at that point.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six Fin 4 arguments are concrete literals, so the kernel evaluates the fold that defines the numerator and the pattern match that defines $Z$, then checks equality with $8\cdot Z$. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the claim by exhaustive fin_cases over all six indices. Each chunk theorem such as this one supplies one (or a block of) decided cells so the assembly does not re-decide the whole $4^6$ space in a single tactic block.
In the broader Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge TT kernel in four dimensions: it pins the discrete numerator against the closed-form $Z$ table before continuum or continuum-limit arguments. It does not itself invoke the forcing chain (T0–T8), $\varphi$, or the eight-tick octave; those enter only at higher layers that consume the certified kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.