e_020201
plain-language theorem explainer
For the six-index slot (0,2,0,2,0,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,0,2,0,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 one chunk of a 256-case kernel certification that the 4D Regge midpoint numerator $m_2^{\mathrm{num}}$ is exactly eight times a sparse explicit integer table $Z$. Both maps take six arguments in $\mathrm{Fin},4$ (edge/face index slots) and return an Int.
The numerator is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each coupling triple. The explicit table $Z$ is a pattern-matched closed form that is nonzero only on a short list of index patterns (e.g. diagonal blocks yield $4$, certain off-diagonal swaps yield $-2$).
Local setting (module doc): prove $m_2^{\mathrm{num}}=8\cdot Z$ case-by-case so a later assembler can recombine the chunks into a single quantified identity.
proof idea
One-line decide proof. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed: the fold that defines the numerator evaluates fully, and the pattern match for the explicit kernel returns a single integer (or zero if unmatched). Lean’s kernel decision procedure checks the resulting integer equality $n=8z$.
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$ by exhausting all six Fin 4 indices and dispatching each concrete cell to a chunk lemma of this form. That global identity is the algebraic backbone of the exact midpoint M2 TT identity in the 4D Regge analysis stack: it replaces a folded coupling sum by a sparse closed form, enabling exact (not approximate) curvature/mass bookkeeping in the gravity sector.
Within Recognition Science this sits in the gravity analysis layer that supports continuum limits and discrete curvature identities consistent with the forced $D=3$ spatial skeleton and eight-tick causal structure; it is computational certification rather than a new forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.