e_033131
plain-language theorem explainer
For the six-index tuple (0,3,3,1,3,1) on Fin 4, the folded M2 numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite these per-tuple decides when assembling the exact 4D Regge midpoint M2 identity. The proof is a single kernel decision on concrete integer arithmetic.
Claim. For indices $a=0$, $b=3$, $c=3$, $d=1$, $i=3$, $j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\cdot Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel on those indices.
background
This module is chunk 3 of a 256-case kernel certification that the midpoint M2 numerator equals eight times an explicit integer table on all six-tuples in $(\mathrm{Fin},4)^6$. The local setting is exact algebraic identities for 4D Regge calculus at the midpoint, not continuum GR.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a contribution term at each entry. The comparison table $Z$ is an explicit pattern-matched integer function on the same six indices (sample clauses give values such as $4$, $-2$, and so on). Both live in the kernel-cert module imported here.
The full quantified identity is assembled downstream by exhausting Fin 4 in each slot; each chunk theorem pins one concrete tuple so the case split can close by reference or decide.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are substituted: the left-hand fold over the coupling list becomes a fixed integer sum, and the right-hand side is eight times the matching clause of the explicit Z table. Lean’s decision procedure discharges the resulting integer equality with no lemmas beyond the definitions of the numerator and the Z table.
why it matters
This is one cell in the 256-case grid that certifies $m_2^{\mathrm{num}}=8Z$ pointwise. Downstream, m2Num_eq_eight_explicitZ states the full universal claim over all $a,b,c,d,i,j:\mathrm{Fin},4$ and closes by nested fin_cases; the chunk theorems supply (or witness) the individual cases.
In the Recognition gravity stack, exact midpoint M2 identities are algebraic scaffolding for discrete curvature and coupling bookkeeping in 4D Regge-type analyses. They do not themselves invoke the forcing chain (T5–T8) or the Recognition Composition Law, but they keep the gravity-side numerics fully certified rather than floating-point. Closing every chunk removes a scaffolding gap in the 4D midpoint kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.