e_312312
plain-language theorem explainer
For the Fin-4 index sextuple (3,1,2,3,1,2), the folded midpoint M2 numerator equals eight times the explicit integer kernel entry. Gravity analysts assembling the 4D Regge midpoint TT identity cite this as one of the exhaustive kernel cases. The proof is a single decide on concrete integer arithmetic.
Claim. For indices $a=3$, $b=1$, $c=2$, $d=3$, $i=1$, $j=2$ in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module sits inside the 4D Regge exact-midpoint M2 TT-identity analysis. The local goal, stated in the module header, is to discharge one chunk of the identity $m_2^{\mathrm{num}}=8\cdot Z$ by kernel decides.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing integer contributions at the six Fin-4 slots. The comparison table $Z$ is an explicit pattern-matched integer function on the same six indices (sample values include $4$ and $-2$ on the diagonal and off-diagonal patterns).
Both objects live in the kernel-certificate module imported here. The present declaration fixes one concrete sextuple and checks the scalar identity at that point.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side by evaluating the fold of contributions at $(3,1,2,3,1,2)$, the right-hand side by evaluating the pattern match for $Z$ and multiplying by $8$. Lean’s kernel decision procedure checks integer equality; no lemmas are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts the identity for every sextuple in $(\mathrm{Fin},4)^6$. Its proof runs nested fin_cases on all six indices and lands on per-case facts of this form. This declaration is the case $(3,1,2,3,1,2)$ inside chunk 13 of that assembly.
In the broader gravity stack, the equality $m_2^{\mathrm{num}}=8Z$ is the algebraic certificate that the discrete midpoint M2 TT kernel matches its closed-form table. That certificate is infrastructure for the Regge-side exact identities used in the Recognition gravity analysis; it does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law, but it clears a finite combinatorial obligation those continuum claims rest on once discretized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.