e_022222
plain-language theorem explainer
For the single multi-index (0,2,2,2,2,2) on Fin 4, the folded coupling numerator equals eight times the explicit integer table entry. Gravity analysts cite it as one atomic case of the 4D Regge midpoint M2–TT kernel identity. The proof is a pure kernel decide on that fixed tuple.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,2,2,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 one chunk of the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on the 4D Regge midpoint kernel. The ambient setting is discrete gravity analysis: six indices in $\mathrm{Fin},4$ label edge/face data for a midpoint contribution.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at the six indices. The comparison object $Z$ is an explicit integer-valued table on the same six indices (pattern-matched closed form, with entries such as $4$, $-2$, and so on).
Chunk 2 holds 256 such kernel decides. Sibling lemmas cover the other fixed tuples in the same block; the full universal statement is assembled downstream by exhausting $\mathrm{Fin},4$ in each slot.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six indices are concrete numerals, so the kernel evaluates the fold that defines the numerator and the pattern match that defines the table entry, then checks equality with $8\cdot Z$. No lemmas are invoked beyond the definitions of the numerator and the explicit table.
why it matters
Parent theorem is the universal identity: for all six indices in $\mathrm{Fin},4$, the numerator equals eight times the explicit table. That assembler introduces the six variables and runs fin_cases on each; each concrete branch lands on a chunk lemma of this form.
In the Recognition gravity stack this is bookkeeping infrastructure for the 4D Regge midpoint M2–TT identity, not a forcing-chain step (T0–T8) or a constants claim. It closes one of the $4^6$ pointwise obligations so the assembled equality can be cited without residual case splits. No open physics question is settled here; the value is machine-checked coverage of a single kernel cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.