e_213321
plain-language theorem explainer
For the six-index tuple (2,1,3,3,2,1) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite this as one cell of the 4^6 case split that certifies the Regge midpoint M2 TT identity in four dimensions. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,\,b{=}1,\,c{=}3,\,d{=}3,\,i{=}2,\,j{=}1$ in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(2,1,3,3,2,1)=8\,Z_{\mathrm{ex}}(2,1,3,3,2,1)$.
background
This module is chunk 9 of a 256-way kernel certification that the four-dimensional Regge midpoint M2 TT numerator agrees with an explicit closed-form integer table. The ambient setting is discrete gravity analysis: edge and face couplings on a 4-simplex skeleton, with all free indices ranging over Fin 4.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each six-index slot. The comparison target $Z_{\mathrm{ex}}$ is an explicit pattern-matched integer function on the same six Fin-4 arguments (sample clauses include values $4$, $-2$, and so on). The claim under audit is one concrete evaluation of the identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete indices $(2,1,3,3,2,1)$ to integers (the fold that defines the numerator versus the pattern match that defines the explicit kernel) and checks equality in the kernel. No lemmas are invoked beyond the two defining defs.
why it matters
Parent consumer is the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in Fin 4 by exhaustive fin_cases and discharges each leaf by a chunk theorem of this form. Without the per-cell equalities, the global numerator-versus-explicit-Z certificate for the Regge midpoint M2 TT identity in 4D does not close.
In the Recognition gravity stack this is pure discrete-analysis scaffolding: it underwrites the algebraic identity used when matching continuum curvature weights to the phi-ladder and eight-tick discrete structure, rather than a new physical law. It touches no open forcing-chain step (T0–T8); it only seals one integer cell of a large decide grid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.