e_313011
plain-language theorem explainer
One kernel cell of the 4D Regge midpoint identity: the numerator mass-squared coupling at multi-index (3,1,3,0,1,1) equals eight times the explicit integer table entry at that cell. Gravity analysts assembling the global m2Num = 8·explicitZ identity cite these cells. The proof is a pure kernel decide on fixed Fin 4 indices.
Claim. For the fixed multi-index $(a,b,c,d,i,j)=(3,1,3,0,1,1)$ in $(\mathrm{Fin}\,4)^6$, the folded numerator coupling $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
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator side $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing local contributions at $(a,b,c,d,i,j)$. The comparison side is an explicit pattern-matched table explicitZ that returns small integers (typically $\pm 2,\pm 4$, or $0$ off the listed patterns).
The module is chunk 13 of a 256-cell decide sweep: each cell asserts $m_2^{\mathrm{num}}=8\cdot Z$ at one concrete multi-index. The local setting is purely combinatorial kernel certification inside the gravity analysis stack, not a continuum GR derivation.
Upstream, both sides are closed definitions in the kernel certificate module; no analytic hypotheses are carried.
proof idea
One-line kernel proof: decide evaluates both sides at the concrete Fin-4 tuple $(3,1,3,0,1,1)$ and checks integer equality. No lemmas are invoked beyond the computable definitions of the folded numerator and the explicit table.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for all six Fin-4 indices by exhaustive fin_cases and discharges each cell with a chunk theorem of this form. That global equality is the certified algebraic core of the Regge-exact midpoint $M_2$ TT identity in 4D inside the gravity analysis layer.
Within Recognition Science this sits in the discrete gravity/Regge bookkeeping that supports continuum limits and dimension-sensitive identities (cf. the $D=3$ spatial forcing landmark at the continuum level). It does not itself touch the J-cost, $\phi$-ladder, or forcing chain; it is infrastructure that keeps the 4D kernel identity fully machine-checked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.