e_021331
plain-language theorem explainer
For the six-index slot (0,2,1,3,3,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the exact midpoint M2 TT identity in 4D Regge calculus. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,3,3,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-case kernel certification that the Regge midpoint numerator $m_2^{\mathrm{num}}$ is identically eight times a sparse explicit table $Z$ on $(\mathrm{Fin},4)^6$. The ambient setting is 4D discrete gravity: edge and face couplings are summed into an integer numerator before any continuum limit.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and accumulating a contribution at each tuple. The comparison target $\mathrm{explicit}Z$ is a pattern-matched integer table on six $\mathrm{Fin},4$ indices (typical nonzero entries are $\pm 2,\pm 4$). Both live in the kernel certificate module imported here.
The full identity is $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$. Exhaustive fin_cases on six indices is split across many one-point lemmas of this form so each decide stays small.
proof idea
One-line decide proof. Both sides reduce to concrete Int values: the left by evaluating the fold of couplingZList at the fixed indices $(0,2,1,3,3,1)$, the right by looking up explicitZ at those same indices and multiplying by 8. No lemmas are invoked beyond kernel reduction of the two definitions.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the universal identity $\forall(a,b,c,d,i,j),, m_2^{\mathrm{num}}=8,Z$ by fin_cases over all six indices and dispatching to these pointwise chunks. That identity is the algebraic core of the exact midpoint M2 TT certificate in 4D Regge analysis: it replaces a summed coupling expression by a sparse closed form, enabling later curvature and continuum checks.
Within Recognition Science gravity work this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8). It does not touch $\phi$, the eight-tick octave, or $J$-cost uniqueness; it only certifies a discrete numerator identity needed before continuum or phenomenological claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.