e_200112
plain-language theorem explainer
For the six-index slot (2,0,0,1,1,2) on Fin 4, the folded coupling numerator equals eight times the explicit integer table entry. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M₂ identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(2,0,0,1,1,2)$ equals $8$ times the explicit closed-form integer at those same indices.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator is obtained by folding a fixed coupling list: start at 0 and add each local contribution for the given multi-index. The explicit map is a finite pattern-matched table of small integers (entries such as $4$, $-2$, and so on).
This module is chunk 8 of a 256-case kernel split whose sole job is to check numerator $= 8\cdot$ explicit table pointwise. The local setting is pure finite enumeration over $(\mathrm{Fin},4)^6$, not continuum GR.
proof idea
One-line computational proof: decide evaluates both sides at the concrete indices $(2,0,0,1,1,2)$ and checks integer equality in the kernel. No algebraic lemmas are invoked; the fold and the table lookup reduce to ground terms.
why it matters
Feeds the assembly theorem that states the identity for every six-tuple: after introducing the six Fin-4 variables, exhaustive fin_cases dispatches to these chunk lemmas (including this one) so that numerator $= 8\cdot$ explicit holds globally.
That global identity is the certified algebraic core of the 4D Regge exact-midpoint $M_2$ TT block in the Gravity analysis stack. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is infrastructure that keeps the discrete curvature bookkeeping exact before continuum limits are discussed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.