e_321103
plain-language theorem explainer
For the six-index slot (3,2,1,1,0,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. 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,2,1,1,0,3)$ equals eight times the explicit integer kernel at the same indices: $N(3,2,1,1,0,3)=8\,Z(3,2,1,1,0,3)$.
background
This module is chunk 14 of a 256-way case split proving that the Regge midpoint $M_2$ numerator equals eight times an explicit integer kernel on all six-tuples of indices in $\mathrm{Fin},4$.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution for each coupling term at the six indices. The closed form $Z=\mathrm{explicitZ}$ is a pattern-matched integer table on those same indices (typical values $\pm 2,\pm 4$, and so on).
The local goal is purely algebraic bookkeeping: for each concrete six-tuple, check $N=8Z$ by evaluation, then reassemble the universal statement by exhaustive fin_cases.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides at the concrete Fin-4 sextuple $(3,2,1,1,0,3)$ and confirms integer equality. No lemmas beyond the definitions of the folded numerator and the explicit kernel table are required.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathrm{Fin},4,; N=8Z$ by running fin_cases over all six indices and dispatching each cell to a chunk decide such as this one.
In the gravity analysis stack this identity is the certified algebraic core of the exact midpoint $M_2$ TT identity in 4D Regge calculus. It is bookkeeping infrastructure rather than a Recognition forcing step (T0–T8), but it locks the discrete curvature numerator to a sparse explicit kernel before continuum or phenomenological claims are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.