e_332002
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (3,3,2,0,0,2) equals eight times the explicit integer table entry. Gravity analysts cite it as one of 256 kernel cells assembling the global m2Num = 8·explicitZ identity. Proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,3,2,0,0,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 closed-form integer $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at the given multi-index. The companion map $\mathrm{explicitZ}$ is a sparse case table of small integers (entries such as $4$, $-2$, and so on) intended as the closed form of that fold.
This module is chunk 15 of a 256-cell kernel partition: each cell fixes one concrete sextuple and asserts $m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$ there. The factor $8$ is the global normalization relating the folded sum to the tabulated values. The surrounding development aims at an exact midpoint identity for the Regge $M_2$ TT sector in four dimensions.
proof idea
Both sides evaluate to concrete integers once the six indices are fixed. The proof is the single tactic decide, which reduces the equality of those integers in the kernel. No algebraic lemmas are invoked; the definitions of the fold and of the case table are unfolded by the decision procedure.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the identity for every sextuple in $(\mathrm{Fin},4)^6$. Its proof introduces the six indices and exhausts them by fin_cases; each concrete goal is discharged by a chunk theorem of this form. Without the full 256-cell cover, the global equality does not close.
In the Recognition gravity stack this global equality is the certified numerator identity behind the exact midpoint $M_2$ TT relation in 4D Regge calculus. It is bookkeeping rather than a forcing-chain step (T0–T8), but it is required scaffolding for any claim that the discrete curvature numerator matches the closed form used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.