e_201200
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,0,1,2,0,0) equals eight times the explicit integer kernel entry there. Gravity analysts cite it as one cell of the 256-case kernel that builds the global m2Num = 8·explicitZ statement. Proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,2,0,0)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of a 256-way case split proving that the 4D Regge midpoint TT numerator equals eight times an explicit integer kernel on every sextuple of indices in $\mathbb{F}_4$.
The numerator $N$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the given indices. The explicit kernel $Z$ is a closed-form integer table on $(\mathbb{F}_4)^6$ (sample values include $4$, $-2$, and so on for listed patterns).
Local setting is pure finite enumeration: no continuum limit, no metric ansatz beyond the discrete midpoint kernel already certified upstream.
proof idea
One-line proof by decide. Lean evaluates both sides as concrete Int values for the fixed sextuple $(2,0,1,2,0,0)$ and checks equality in the kernel. No lemmas are invoked beyond the definitions of the folded numerator and the explicit table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall$ indices in $(\mathbb{F}_4)^6$, $N=8Z$, by six nested fin_cases that discharge each cell (including this one). That global identity is the algebraic core of the Regge exact midpoint M2 TT identity in 4D within the Gravity analysis stack.
In the broader Recognition framework this is bookkeeping infrastructure for discrete curvature/TT projections, not a forcing-chain landmark (T5–T8). It closes one of 256 decide obligations so the quantified midpoint identity can be cited without residual case debt.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.