e_313212
plain-language theorem explainer
Concrete integer identity: the folded M2 numerator coupling at Fin-4 indices (3,1,3,2,1,2) equals eight times the explicit kernel value at those indices. Gravity analysts cite it as one case in the 4D Regge midpoint M2TT numerator certification. The proof is a single kernel decide on the unfolded integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,2,1,2)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit kernel entry: $m_2^{\mathrm{num}}(3,1,3,2,1,2)=8\,Z(3,1,3,2,1,2)$.
background
This module is chunk 13 of the certification that the 4D Regge exact-midpoint M2TT numerator equals eight times an explicit integer kernel on every sextuple of Fin 4 indices. The ambient setting is discrete gravity analysis: couplings assembled from a fixed list, then compared to a closed-form table.
Upstream, m2Num a b c d i j is the fold of contrib over couplingZList, yielding an Int. The companion explicitZ is a pattern-matched integer table on six Fin 4 arguments (sample clauses send e.g. (0,0,1,1,2,2) to 4 and (0,0,1,2,1,2) to -2). The claim is one pointwise instance of m2Num = 8 · explicitZ.
Sibling theorems in the same chunk discharge neighboring sextuples the same way; together they feed the exhaustive assembly.
proof idea
One-line proof by decide. After reducing the six concrete Fin 4 literals, both sides are closed integer expressions: the left from the fold definition of the numerator, the right from the matching clause (or default) of the explicit kernel. The kernel decides the resulting Int equality; no lemmas beyond the two definitions are required.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states the identity for every (a,b,c,d,i,j) : Fin 4, proved by nested fin_cases. This declaration is one discharged cell in that case tree (chunk 13 of the 256-decide split). Without the pointwise facts, the universal numerator identity does not close.
In the Recognition gravity stack the identity is bookkeeping infrastructure for the Regge midpoint M2TT analysis in 4D: it certifies that the assembled coupling numerator matches the explicit kernel used downstream. It does not itself invoke the forcing chain (T5–T8), RCL, or the phi ladder; it is a pure integer certification step inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.