e_023010
plain-language theorem explainer
Pointwise kernel identity: the folded Regge numerator at index sextuple (0,2,3,0,1,0) equals eight times the explicit integer table at those indices. Gravity analysts cite it when assembling the full m2Num = 8·explicitZ identity over (Fin 4)^6. Proof is a single kernel decide on concrete integers.
Claim. For the index sextuple $(0,2,3,0,1,0)\in(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit closed-form table entry: $m_2^{\mathrm{num}}(0,2,3,0,1,0)=8\,Z_{\mathrm{expl}}(0,2,3,0,1,0)$.
background
This module is chunk 2 of a 256-way kernel certification that the 4D Regge midpoint $M_2$ numerator equals eight times an explicit integer table. The ambient setting is discrete gravity analysis: couplings on oriented 4-simplices with indices in $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating each term's contribution at the six indices. The comparison object $Z_{\mathrm{expl}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern match (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$, and so on).
The local claim is one concrete sextuple in that table-vs-fold comparison. Sibling lemmas cover the other index combinations in the same chunk.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold of couplingZList at fixed indices $(0,2,3,0,1,0)$; the right-hand side looks up explicitZ at those indices and multiplies by 8. Lean’s kernel decision procedure discharges the resulting integer equality with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases on all six indices. Each chunk lemma such as this one supplies one decided cell so the universal identity is a pure case split rather than a symbolic expansion of the fold.
In the Recognition gravity stack this identity is infrastructure for the exact midpoint $M_2$ TT analysis in 4D Regge calculus. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is a finite combinatorial certificate underneath those continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.