e_201231
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,0,1,2,3,1) equals eight times the explicit Z-table entry. Gravity analysts cite it when assembling the full 4D Regge midpoint m2-numerator certificate. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,2,3,1)$ in $(\mathbb{F}_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
This module is one chunk of the 4D Regge-exact midpoint certificate that the mass-squared numerator kernel equals eight times a sparse explicit integer table. The ambient setting is discrete gravity analysis on four-valued face and edge labels (Fin 4).
The numerator m2Num is defined by folding a fixed coupling list and summing a local contribution at each six-index. The comparison table explicitZ is a pattern-matched integer function on the same six indices (typical values $\pm 2,,4$, and zero off the listed patterns).
Chunk 8 holds 256 such pointwise equalities; each is an independent closed integer identity used later by exhaustive case split on all six coordinates.
proof idea
One-line kernel proof: decide evaluates both sides as concrete Int expressions (the fold of m2Num at the fixed six-tuple versus 8 * explicitZ at the same tuple) and discharges equality by computation. No lemmas are invoked beyond the definitions of the two sides.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathbb{F}_4)^6$ by exhaustive fin_cases. That global equality is the algebraic core of the Regge-exact midpoint $M_2$ TT-identity certificate in 4D: it replaces a folded coupling sum by a sparse explicit table, making downstream curvature and mass-kernel identities decidable.
Within Recognition gravity analysis this is bookkeeping, not a forcing-chain step (T0–T8), but it is required scaffolding for exact discrete-gravity identities that sit under the continuum limit. Closing all 256 chunks removes a large block of computational obligations from the parent certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.