e_320231
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (3,2,0,2,3,1) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the 4D Regge midpoint M2–TT numerator identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,0,2,3,1)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the M2–TT numerator is built by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums contribution terms over that list. The companion table $Z$ is an explicit integer-valued function on six $\mathrm{Fin},4$ indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The local module is chunk 14 of a kernel-decide sweep whose goal is the pointwise relation $m_2^{\mathrm{num}}=8Z$ on the full $4^6$ index cube. Each chunk theorem pins one concrete six-tuple so the assembler can recombine them without re-running the fold.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(3,2,0,2,3,1)$ in the kernel and checks integer equality. No lemmas beyond the definitions of the fold numerator and the explicit table are required.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the claim by exhaustive fin_cases over the six indices. That global identity is the algebraic backbone of the exact midpoint M2–TT relation in the 4D Regge gravity analysis. Within Recognition Science it sits in the gravity sector that must match continuum curvature identities once the discrete eight-tick and $D=3$ forcing (T7–T8) fix the lattice geometry; it does not itself touch the J-cost or $\phi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.