e_311311
plain-language theorem explainer
For the six-index slot (3,1,1,3,1,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel point-checks that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the midpoint Regge numerator $m_2^{\mathrm{num}}(3,1,1,3,1,1)$ equals $8$ times the explicit kernel integer $Z(3,1,1,3,1,1)$.
background
This module is chunk 13 of a 256-way case split proving that the folded midpoint numerator equals eight times a closed-form kernel on every 4D index tuple. The ambient setting is exact midpoint analysis for Regge-type gravity couplings in four dimensions.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those six Fin-4 indices. The comparison target $\mathrm{explicitZ}$ is a piecewise integer table on the same six indices (sample values include $4$, $-2$, and other small integers on the listed patterns).
The global claim is $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$. Each chunk theorem discharges one concrete hexuple so the assembler can finish by exhaustive fin_cases.
proof idea
One-line kernel proof: decide evaluates both sides at the concrete indices $(3,1,1,3,1,1)$ and checks integer equality. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (fold of contributions) and $\mathrm{explicitZ}$ (lookup table).
why it matters
Feeds the assembler theorem $m_2^{\mathrm{num}}=8,\mathrm{explicitZ}$ for all Fin-4 indices, which is the parent identity in ReggeExactMidpointM2TTIdentity4DM2NumAssemble. That parent introduces the six indices and closes by nested fin_cases, each leaf a chunk equality of this form.
In the gravity analysis stack these pointwise numerator identities underwrite the exact midpoint M2/TT kernel certification. They are bookkeeping, not a new physical law: they lock the algebraic reduction that later continuum or continuum-limit arguments rely on when comparing discrete Regge couplings to continuum curvature weights.
No Recognition forcing-chain step (T5–T8) is restated here; the link is infrastructural support for the 4D gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.