e_122011
plain-language theorem explainer
For the six-index slot (1,2,2,0,1,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint Regge M2 identity cite this as one of the 256 kernel decides. The proof is a single kernel decision (`decide`) on concrete integers.
Claim. For indices $a=1,b=2,c=2,d=0,i=1,j=1$ 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
This module is chunk 6 of a 256-way case split proving that the Regge midpoint M2 numerator equals eight times an explicit integer table on all six-tuples in $(\mathrm{Fin},4)^6$. The local claim is purely arithmetic: evaluate both sides at one fixed tuple.
The numerator $N$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling entry at the given indices. The table $Z$ is a pattern-matched integer function on six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for distinguished index patterns).
The surrounding Gravity.Analysis development certifies an exact midpoint identity for the 4D Regge M2 tensor; these chunk lemmas discharge the finite case analysis that equates the folded form to the closed table.
proof idea
One-line proof by decide. Both sides are closed integer expressions at concrete Fin 4 values (coerced to the matching constructors), so the kernel reduces the equality to true by computation. No lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
Feeds the assembly 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, invoking one chunk equality per cell. Without the full 256-cell cover, the exact midpoint M2 identity in 4D Regge calculus stays conditional on the numerator-table match.
In the Recognition gravity stack this is bookkeeping infrastructure rather than a forcing-chain step (not T0–T8): it locks the discrete curvature/mass kernel so later continuum or phenomenological claims rest on a fully decided finite identity. Sibling chunks (e_120000 and neighbors) play the same role for other index tuples.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.