e_202001
plain-language theorem explainer
At multi-index (2,0,2,0,0,1) the folded Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it as one of the 256 concrete kernel cells that assemble into the global identity. The proof is a single kernel decide on fixed Fin-4 indices.
Claim. For indices $(a,b,c,d,i,j)=(2,0,2,0,0,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel on six $\mathbb{F}_4$ legs.
background
This module sits in the 4D Regge exact-midpoint analysis for the mass-squared TT identity. The local goal, stated in the module header, is to verify $m_2^{\mathrm{num}}=8\cdot Z$ on one chunk of the $4^6=4096$ index space by discharging 256 concrete kernel cells.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it sums the contribution of each coupling term at the six $\mathbb{F}_4$ indices. The comparison target $Z$ is an explicit piecewise-integer function on the same six indices (sample values include $4$, $-2$, and so on on the listed patterns).
Chunk 8 is one block of those decides. The present cell fixes the multi-index to $(2,0,2,0,0,1)$.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(2,0,2,0,0,1)$. The left side runs the fold that defines the numerator; the right side multiplies the explicit kernel value by eight. No lemmas are invoked beyond kernel reduction of integer arithmetic on fixed indices.
why it matters
The parent theorem is the universal assembly statement: for every $(a,b,c,d,i,j)\in(\mathbb{F}_4)^6$, the numerator equals eight times the explicit kernel. That proof introduces all six indices and runs fin_cases on each, so each leaf is exactly one of these chunk theorems.
In the gravity stack this identity is the certified algebraic core of the 4D Regge midpoint mass-squared TT relation. Closing the 256-cell chunks removes a scaffolding gap between the folded coupling definition and the closed-form kernel used downstream. It does not itself invoke the Recognition forcing chain (T5–T8) or the RCL; it is pure discrete tensor algebra supporting the continuum gravity claims built on top.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.