e_021023
plain-language theorem explainer
For the six Fin-4 indices (0,2,1,0,2,3), the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic cell in the 4D Regge midpoint M2 identity. The proof is a pure kernel decide on the two integer expressions.
Claim. With indices $a=0$, $b=2$, $c=1$, $d=0$, $i=2$, $j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $N$ (Lean m2Num) is the fold of a fixed coupling list: each term contributes an integer via a local contribution function, and the fold starts at zero. The closed form $Z$ (Lean explicitZ) is a pattern-matched table of small integers (entries such as $4$, $-2$, and so on) on the same six-index domain.
The module is one chunk of a 256-cell kernel certification that $N=8Z$ pointwise. Chunk 2 packages a block of those pointwise equalities so the global assembly can discharge every index tuple by case split rather than by a single monolithic decide.
proof idea
One-line computational proof: decide evaluates both sides as concrete integers (the fold for $N$ and the table lookup for $Z$) and checks equality. No lemmas are invoked beyond the definitions of the two maps.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j., N=8Z$ and proves it by exhaustive fin_cases on all six indices, routing each cell to a chunk equality such as this one. That identity is the algebraic backbone of the exact midpoint M2/TT relation in the 4D Regge gravity analysis inside Recognition Science. It is bookkeeping infrastructure for the discrete curvature side, not a forcing-chain landmark (T5–T8), but without the pointwise $N=8Z$ cells the midpoint assembly does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.