e_213203
plain-language theorem explainer
For the six-index tuple (2,1,3,2,0,3) on Fin 4, the Regge midpoint m2 numerator equals eight times the explicit Z coupling at those indices. Gravity analysts cite it as one cell of the 256-point kernel identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the midpoint Regge numerator satisfies $m_2^{\mathrm{num}}(2,1,3,2,0,3)=8\,Z_{\mathrm{expl}}(2,1,3,2,0,3)$.
background
This module is chunk 9 of a 256-case kernel certification that the discrete midpoint m2 numerator equals eight times an explicit integer coupling table on $(\mathrm{Fin},4)^6$. The ambient setting is 4D Regge-calculus analysis of the TT midpoint identity.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a local contribution at each table entry. The comparison object $Z_{\mathrm{expl}}$ is a closed-form integer pattern on six Fin-4 indices (sample values include $4$, $-2$, and so on for the listed index patterns).
The full identity is $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$. Exhaustive casework on Fin 4 yields $4^6=4096$ atomic goals in the assembler; this file discharges a 256-sized decide block, of which the present declaration is one cell.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are fixed to 2,1,3,2,0,3, so the kernel equality checker closes the goal with no lemmas beyond the definitions of the numerator fold and the explicit coupling table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple by exhaustive fin_cases and consumes the chunk decides. That global equality is the certified algebraic core of the 4D Regge exact-midpoint M2 TT identity: the discrete numerator is exactly eight copies of the explicit Z table, with no residual defect on the finite index set.
Inside Recognition gravity analysis this is bookkeeping, not a new physical law, but it locks the discrete curvature/coupling arithmetic that later continuum or continuum-limit arguments rely on. It does not itself invoke the forcing chain (T5–T8), RCL, or the phi ladder; it is pure finite-index integer identity supporting the Regge sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.