e_211002
plain-language theorem explainer
Pointwise check that the Regge midpoint mass-squared numerator equals eight times the explicit Z-kernel at multi-index (2,1,1,0,0,2). Gravity analysts cite it only as one cell of the 256-way kernel table. The proof is a pure `decide` on concrete integer arithmetic after unfolding the fold and the case table.
Claim. For indices $(a,b,c,d,i,j)=(2,1,1,0,0,2)$ 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 $Z(a,b,c,d,i,j)$.
background
This module is chunk 9 of a 256-cell kernel certification that the midpoint Regge identity $m_2^{\mathrm{num}}=8,Z$ holds on every 4D multi-index. The ambient setting is discrete gravity analysis: couplings on a 4-simplex lattice with values in $\mathbb{F}_4$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a contribution term at the six indices. The comparison object $Z$ is an explicit case-table on $(\mathrm{Fin},4)^6\to\mathbb{Z}$ (e.g. $(0,0,1,1,2,2)\mapsto 4$, off-diagonal pairs $\mapsto -2$). Both live in the kernel certificate module imported here.
The full quantified identity is assembled downstream by exhausting all six $\mathrm{Fin},4$ coordinates; each chunk theorem discharges one concrete cell.
proof idea
One-line computational proof: decide. Lean unfolds $m_2^{\mathrm{num}}$ at the fixed indices $(2,1,1,0,0,2)$, evaluates the fold of contributions to an integer, looks up $Z(2,1,1,0,0,2)$ in the explicit case table, and checks equality with $8$ times that value by native integer decision.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by nested fin_cases over all six indices. Each chunk such as this one is a named cell so the 256 kernel decides stay modular and inspectable.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge mass-squared structure in 4D, not a forcing-chain step (T0–T8). It closes a pure algebraic certificate: once every cell matches, the global numerator–kernel relation is unconditional. No open scaffold remains on this cell; the residual work is only the sibling cells and the assembler.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.