e_213012
plain-language theorem explainer
For multi-index (2,1,3,0,1,2) on Fin 4, the folded coupling numerator equals eight times the explicit integer table. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one kernel case among the chunked pointwise checks. Proof is a single kernel decide after unfolding the fold and the pattern match.
Claim. For indices $a=2$, $b=1$, $c=3$, $d=0$, $i=1$, $j=2$ in $\mathrm{Fin}\,4$, the coupling-fold numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(2,1,3,0,1,2)=8\,Z_{\mathrm{expl}}(2,1,3,0,1,2)$.
background
In the 4D Regge exact-midpoint analysis, the numerator m2Num accumulates integer contributions by folding a fixed coupling list with a local contrib term over six coordinates in Fin 4. The companion explicitZ is a pattern-matched integer table that records the intended closed form of that sum (scaled by 1/8) at each multi-index.
This module is chunk 9 of the kernel that discharges the pointwise identity numerator = 8 · explicit table by 256 decide steps. The local setting is pure integer arithmetic on Fin 4 labels; no continuum limit, curvature hypothesis, or Recognition constant enters the statement.
proof idea
One-line kernel decision. Lean unfolds the fold-definition of the numerator and the pattern match of the explicit table at the concrete indices (2,1,3,0,1,2), reduces both sides to Int literals, and decide closes the equality. No lemmas beyond the two definitions are applied.
why it matters
Feeds the parent universal statement that the numerator equals eight times the explicit table for every six-tuple in Fin 4. That parent is proved by nested fin_cases over all indices and consumes each chunk case such as this one. The factor-of-eight identity is discrete bookkeeping toward the exact midpoint M2TT identity in 4D Regge calculus inside the Recognition gravity stack. It does not itself touch the forcing chain (T0–T8), the J-cost, or the phi ladder; it only certifies one tensor-algebra cell used by the continuum claim upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.