e_320323
plain-language theorem explainer
Pointwise identity: the folded 4D midpoint numerator at multi-index (3,2,0,3,2,3) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full m2Num = 8·explicitZ kernel. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,0,3,2,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit closed-form integer $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge midpoint M2TT kernel certification: verify that the folded numerator equals eight times an explicit integer table, across all $4^6=4096$ index tuples, split into decide-sized pieces (here chunk 14, 256 decides).
The numerator $N$ is defined by folding a fixed coupling list, accumulating a local contribution at each six-index slot. The table $Z$ is a pattern-matched closed form on $(\mathbb{F}_4)^6\to\mathbb{Z}$ (sample clauses: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and so on). Both live in the kernel certificate module.
The local claim is the single instance at $(3,2,0,3,2,3)$. Sibling theorems cover the other tuples in the chunk.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed: the left side evaluates the fold of contributions; the right side looks up (or defaults) the explicit table and multiplies by 8. Lean’s kernel decision procedure discharges the resulting integer equality with no lemmas or rewriting.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhausting all Fin 4 cases. That global identity is the algebraic core of the exact 4D midpoint M2TT certificate in the Regge gravity analysis stack.
In the Recognition framework this sits on the gravity side of the discrete geometric calculus (eight-tick / $D=3$ landmarks sit upstream in the forcing chain; here the work is concrete 4-index tensor bookkeeping). Closing every chunk removes scaffolding from the midpoint identity and lets downstream curvature and continuum-limit arguments quote a fully proved numerator formula rather than a table of sorries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.