e_101123
plain-language theorem explainer
For the six Fin-4 indices (1,0,1,1,2,3), the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2TT identity. The proof is a pure kernel decide on the concrete integers.
Claim. For indices $a=1$, $b=0$, $c=1$, $d=1$, $i=2$, $j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 4 of a 256-case kernel certification that the midpoint numerator of the 4D Regge M2TT identity is exactly eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, labelling the four spacetime directions that appear in the discrete curvature couplings.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term evaluated at the six indices. The companion table $Z$ is a total function on six $\mathrm{Fin},4$ arguments that returns a small integer (typical values $\pm 2,,4$, and zero off the listed patterns).
The local claim is the single sextuple $(1,0,1,1,2,3)$. Sibling theorems cover the other combinations in the same chunk; the assemble theorem glues all of them.
proof idea
One-line computational proof: decide evaluates both sides on the concrete Fin-4 sextuple. The left-hand side reduces by unfolding the fold over the coupling list; the right-hand side reduces by pattern-matching the explicit kernel table (or returning the default zero). Equality of the resulting integers is decided in the kernel.
why it matters
Feeds the universal identity m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and is proved by exhaustive fin_cases on all six indices, each case discharging to a chunk theorem of this form.
That identity is part of the exact midpoint analysis for the 4D Regge M2TT sector in the Gravity domain of Recognition Science. It certifies that the discrete curvature numerator collapses to a sparse, explicitly tabulated integer kernel, which is the algebraic backbone needed before continuum or continuum-limit comparisons.
No forcing-chain landmark (T5–T8) is directly invoked here; the result is pure discrete-gravity bookkeeping inside the Regge exact-midpoint pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.