e_311232
plain-language theorem explainer
For the single multi-index (3,1,1,2,3,2) on Fin 4, the folded coupling numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts cite it as one of the 256 decide-certified cells that assemble the exact midpoint M2–TT identity in 4D Regge calculus. The proof is a pure kernel decision on integer arithmetic.
Claim. For indices $a=3,b=1,c=1,d=2,i=3,j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2(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 13 of a 256-cell certification that the 4D Regge midpoint numerator equals eight times an explicit sparse kernel. The ambient setting is discrete gravity: edge and hinge couplings on a 4-simplex skeleton, with all index legs valued in Fin 4.
The numerator m2Num is defined by folding a fixed coupling list: it sums contrib t a b c d i j over every term t in couplingZList, starting from 0. The comparison object explicitZ is a total function Fin 4^6 → ℤ given by a finite pattern match (nonzero only on a short list of index patterns such as (0,0,1,1,2,2) ↦ 4 and (0,0,1,2,1,2) ↦ −2).
The local claim is the instance of m2Num = 8·explicitZ at the concrete six-tuple (3,1,1,2,3,2). Sibling theorems cover the other tuples in the same chunk.
proof idea
One-line proof by decide. Lean reduces both sides to concrete integers: the left-hand side by evaluating the fold of contrib over couplingZList at the fixed indices, the right-hand side by matching explicitZ (or returning the default 0). Equality of the resulting ℤ values is decided by the kernel; no lemmas are invoked.
why it matters
The parent theorem is m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in Fin 4 and is proved by exhaustive fin_cases on each coordinate. Each case obligation is discharged by a chunk theorem of this form; this declaration supplies the cell (3,1,1,2,3,2).
In the Recognition gravity stack the identity is the exact algebraic core of the midpoint M2–TT comparison in 4D Regge calculus. It converts a summed coupling expression into a sparse closed-form kernel, which is the computational bottleneck for later continuum and continuum-limit arguments. The module header records the design: 256 kernel decides, chunked for compile-time control. No open scaffolding remains on this cell; it is a finished decide certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.