e_312302
plain-language theorem explainer
Pointwise identity: the midpoint Regge mass-squared numerator at multi-index (3,1,2,3,0,2) equals eight times the explicit integer kernel value. Gravity analysts cite it when assembling the full 4D m2Num = 8·Z certificate. The proof is a single kernel decide on concrete integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,3,0,2)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel on six $\mathbb{F}_4$ indices.
background
This module is chunk 13 of a 256-case kernel certification that the midpoint Regge mass-squared numerator equals eight times a closed-form integer table. The ambient setting is 4D discrete gravity analysis: six indices each run over $\mathbb{F}_4$ (the type Fin 4), labeling edge and simplex data in the Regge calculus midpoint scheme.
Upstream, m2Num is defined by folding a fixed coupling list and summing a local contribution at the six indices; it is an integer. The companion explicitZ is a pattern-matched integer table on the same six indices (sample clauses include values $4$, $-2$, and so on). The claim under audit is one concrete cell of the asserted equality $m_2^{\mathrm{num}}=8Z$.
Sibling declarations in the same chunk cover neighboring multi-indices; together they feed a single assembly theorem that quantifies over all of $(\mathbb{F}_4)^6$.
proof idea
One-line proof: decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed at $(3,1,2,3,0,2)$, so the kernel discharges the equality by evaluation. No lemmas are invoked beyond the definitions of the folded numerator and the explicit table.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ in the assemble module, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is the leaf that a corresponding case of that case-split lands on.
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint Regge $M^2$ / TT analysis in 4D: it certifies that the numerator built from couplings matches the closed form used downstream. It does not itself invoke the forcing chain (T5–T8), RCL, or the $\varphi$-ladder; those enter at higher layers that consume the certified kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.