e_313122
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (3,1,3,1,2,2) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full 4D midpoint M2TT numerator certificate. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,1,2,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-way kernel split proving that the folded 4D Regge midpoint numerator agrees with an explicit closed-form integer table, scaled by eight. The ambient setting is the exact midpoint M2TT identity in discrete gravity analysis.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each list entry for the six $\mathrm{Fin},4$ indices. The comparison target $\mathrm{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite case table (e.g. $(0,0,1,1,2,2)\mapsto 4$, several sign-flipped $-2$ patterns, and so on).
Each chunk theorem fixes one concrete six-tuple and asserts the scaled equality at that point only. Upstream definitions supply both sides; no analytic continuum limit is involved at this layer.
proof idea
One-line computational proof: decide evaluates both sides as concrete integers (the fold of m2Num at $(3,1,3,1,2,2)$ and $8\cdot\mathrm{explicitZ}$ at the same indices) and discharges the propositional equality by kernel decision. No lemmas beyond the two defining defs are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):\mathrm{Fin},4$ by exhausting cases. That global certificate is the algebraic backbone of the Regge exact-midpoint M2TT numerator identity in 4D discrete gravity inside the Recognition Science gravity stack.
The chunking (256 decides) keeps each goal tiny for the kernel while still covering the full finite index set. It does not itself touch continuum GR, the forcing chain T0–T8, or the phi-ladder mass formula; it is pure finite combinatorial bookkeeping supporting the discrete curvature side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.