e_312123
plain-language theorem explainer
Single kernel point of the 4D midpoint Regge identity: the folded mass-squared numerator at indices (3,1,2,1,2,3) equals eight times the explicit integer coupling Z at those same indices. Gravity analysts cite it only as one of the 256 Fin-4 cases glued by the assembly theorem. The proof is a pure `decide` on closed integer arithmetic.
Claim. For the index sextuple $(a,b,c,d,i,j)=(3,1,2,1,2,3)$ with each index 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 is chunk 13 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of indices in $\mathrm{Fin},4$. The ambient setting is the exact midpoint identity for the 4D Regge mass-squared numerator in the Recognition gravity analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it sums a local contribution at each list entry for the six indices. The comparison object $\mathrm{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern table (typical nonzero values are $\pm 2,\pm 4$). Both live in the kernel certificate module imported by this chunk.
The local claim is only the single point $(3,1,2,1,2,3)$; neighboring declarations cover the other table entries in the same style.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the integer equality. The left-hand side evaluates the fold that defines the numerator at the concrete indices; the right-hand side multiplies the table value of the explicit kernel by eight. No lemmas are invoked beyond the decidable equality of the resulting Int literals.
why it matters
The parent theorem is m2Num_eq_eight_explicitZ, which states the identity for every $a,b,c,d,i,j:\mathrm{Fin},4$ and discharges the universal quantifier by nested fin_cases. Each chunk theorem such as this one supplies one concrete case of that split (module doc: "256 kernel decides").
In the broader Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge calculus in four dimensions: it certifies that the folded numerator matches the closed-form coupling table up to the universal factor eight. It does not itself touch the forcing chain (T0–T8), the J-cost, or the $\varphi$-ladder; it is pure discrete linear-algebra support under the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.