e_010023
plain-language theorem explainer
For the six-index slot (0,1,0,0,2,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(0,1,0,0,2,3)$ equals eight times the explicit integer kernel at the same indices: $N(0,1,0,0,2,3)=8\,Z(0,1,0,0,2,3)$.
background
This module is chunk 1 of a 256-case kernel certification that the folded 4D Regge midpoint numerator equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels $0,1,2,3$.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution for each coupling triple at the six indices. The table $Z=\mathrm{explicitZ}$ is a pattern-matched integer function on six $\mathrm{Fin},4$ arguments, nonzero only on a short list of symmetry-related slots (e.g. $4$ on diagonal-type pairs, $-2$ on crossed pairs).
The local claim is the equality $N=8Z$ at one concrete six-tuple. Sibling theorems cover the other tuples in the same chunk; the assembler later quantifies over all of $\mathrm{Fin},4^6$.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold of contrib over couplingZList at $(0,1,0,0,2,3)$; the right-hand side multiplies the pattern value of explicitZ at those indices by $8$. Lean’s decision procedure checks integer equality, so no algebraic rewriting is needed.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ by exhaustive fin_cases. That identity is the certified numerator half of the 4D Regge exact-midpoint M2TT kernel used in the gravity analysis stack.
In the Recognition framework this sits in the discrete gravity / Regge calculus layer that supports continuum limits and effective Newtonian structure, downstream of the forcing chain’s $D=3$ and eight-tick scaffolding. It does not itself touch $\phi$-ladder masses or $\alpha$; it is pure finite-index arithmetic closing a kernel certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.