e_231012
plain-language theorem explainer
For the six-index slot (2,3,1,0,1,2) on Fin 4, the folded Regge coupling numerator equals eight times the explicit integer table entry. Gravity analysts cite it as one atomic case of the 4D midpoint M2TT identity. The proof is a single kernel `decide` on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the folded coupling numerator and $Z$ for the explicit integer table, one has $N(2,3,1,0,1,2)=8\,Z(2,3,1,0,1,2)$.
background
In the 4D Regge exact-midpoint analysis, the numerator m2Num is the integer obtained by folding a fixed coupling list: each term contributes an integer depending on six Fin-4 indices, and the fold starts at 0. The companion table explicitZ is a closed-form integer function of the same six indices, defined by a finite pattern of cases (e.g. diagonal blocks map to 4, certain off-diagonal pairs to -2).
This module is chunk 11 of the 256 kernel decides that fix the first two indices at $(2,3)$ and exhaust the remaining four. The local claim is the pointwise identity numerator $= 8\cdot$ table at one concrete multi-index inside that chunk.
Upstream, only the two definitions are needed: the fold that builds the numerator and the case table that supplies the right-hand side.
proof idea
One-line computational proof: by decide. Lean reduces both sides to concrete integers (the fold over the coupling list on the left, the matching table clause on the right) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the numerator and the explicit table.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts the identity for every six-tuple in Fin 4 by nested fin_cases. Each leaf is one of these chunk theorems; this declaration discharges the leaf $(2,3,1,0,1,2)$.
That global identity is the algebraic certificate that the midpoint M2TT numerator factors as eight times a sparse explicit integer kernel in 4D Regge calculus. Inside Recognition Science gravity work it is bookkeeping infrastructure for the exact discrete curvature identities, not a forcing-chain step (T0–T8) or a constants claim. It closes one of the 256 decide obligations in the $(a,b)=(2,3)$ block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.