e_112203
plain-language theorem explainer
At multi-index (1,1,2,2,0,3) the Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it as one of the 256 concrete kernel checks that assemble into the global m2Num = 8·explicitZ identity. The proof is a single decide on fixed Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(1,1,2,2,0,3)$ in $(\mathbb{F}_4)^6$, 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 5 of a 256-way case split proving that the midpoint Regge mass-squared numerator coincides with eight times an explicit integer kernel on every 4D multi-index. The ambient setting is discrete gravity analysis: couplings on a 4-simplex lattice with Fin-4 labels.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a contribution functional at the six indices. The comparison object explicitZ is a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a finite pattern of integer values (typical entries $\pm 2,,4$, and zeros elsewhere).
The local claim is only the single tuple $(1,1,2,2,0,3)$. Sibling theorems cover the other tuples in the same chunk.
proof idea
Both sides evaluate to concrete integers once the six Fin-4 arguments are fixed. The tactic decide runs the kernel decision procedure on that closed integer equality and closes the goal. No algebraic rewriting or upstream lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and explicitZ are required.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges it by exhaustive fin_cases on all six indices. Each concrete residue such as this one supplies one decided cell of that case tree.
In the Recognition gravity stack these kernel identities underwrite the exact midpoint Regge mass-squared analysis in 4D. They are bookkeeping, not a new physical law: they certify that the folded coupling definition matches the closed-form integer table used downstream. No forcing-chain landmark (T5–T8, RCL, $\phi$) is touched directly; the result is pure discrete-gravity algebra inside the 4D Regge sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.