e_123203
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (1,2,3,2,0,3) equals eight times the explicit integer table at those indices. Gravity analysts cite it as one kernel cell in the 4D midpoint M2–TT certificate. The proof is a pure `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,3,2,0,3)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(1,2,3,2,0,3)=8\,Z(1,2,3,2,0,3)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at those indices. The companion $Z(a,b,c,d,i,j)$ is an explicit pattern-matched integer table (e.g. $4$, $-2$, and sparse defaults) that is meant to be the closed form of that fold, up to a universal factor of $8$.
This module is chunk 6 of a 256-cell kernel certificate: each cell fixes one concrete sextuple and asserts $N=8Z$ there. The local setting is purely combinatorial over $\mathrm{Fin},4$; no continuum limit or curvature hypothesis enters the cell proofs.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six indices are literals, so the decision procedure discharges equality without lemmas or case splits inside this declaration.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases over $\mathrm{Fin},4$. Each chunk cell such as this one is a named witness the assembler (or the kernel cert infrastructure) can rely on when the six-fold case split bottoms out. In the broader Gravity track this identity is bookkeeping for the exact midpoint M2–TT relation in 4D Regge calculus; it does not itself invoke Recognition landmarks (T5–T8, RCL, $\varphi$), but it hardens the discrete curvature side those landmarks later meet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.