e_311201
plain-language theorem explainer
For the six-index slot (3,1,1,2,0,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over all 4^6 index tuples. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(a,b,c,d,i,j)=(3,1,1,2,0,1)$ equals eight times the explicit integer kernel at those same indices: $N(3,1,1,2,0,1)=8\,Z(3,1,1,2,0,1)$.
background
This module is one chunk in a 256-way case split proving that the Regge midpoint $M_2$ numerator equals eight times an explicit integer kernel on every 4D multi-index. The ambient setting is discrete gravity analysis: couplings on Fin 4 indices are summed into a numerator, then matched to a closed table.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list and accumulating a contribution at each six-tuple $(a,b,c,d,i,j)$. The kernel $Z=\mathrm{explicitZ}$ is a pattern-matched integer table on the same six Fin-4 arguments (typical entries $\pm 2,\pm 4$, and zero off the listed patterns).
Chunk 13 isolates one concrete six-tuple so the global identity can be reassembled by exhaustive fin_cases rather than a single monolithic decide.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side evaluates the fold that defines the numerator at $(3,1,1,2,0,1)$, the right-hand side multiplies the table lookup for the explicit kernel by eight. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and discharges the claim by nested fin_cases over all six Fin-4 indices, each leaf a chunk identity of this form. That global equality is the certified algebraic core of the Regge exact-midpoint $M_2$ TT identity in 4D inside the Gravity analysis stack.
In the broader Recognition framework this sits in the discrete-gravity / Regge calculus layer that supports continuum limits and curvature bookkeeping, downstream of the forcing chain’s $D=3$ spatial result and the eight-tick discrete time structure. It does not itself touch $J$-uniqueness or the $\phi$-ladder mass formula; it is pure index algebra closing a numerator–kernel match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.