e_310021
plain-language theorem explainer
For the six-index slot (3,1,0,0,2,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. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(3,1,0,0,2,1)$ equals eight times the explicit integer kernel at the same slot: $N(3,1,0,0,2,1)=8\,Z(3,1,0,0,2,1)$.
background
This module is one certified chunk of the 4D Regge exact-midpoint M2–TT identity: the claim that the folded numerator m2Num equals eight times a sparse explicit integer table explicitZ on every six-tuple of Fin-4 indices. The module header states the local goal as "m2Num = 8·explicitZ, chunk 13 (256 kernel decides)."
m2Num a b c d i j is defined by folding a fixed coupling list, accumulating integer contributions at those indices. explicitZ is a pattern-matched Int-valued kernel on the same six Fin-4 arguments (nonzero only on a short list of index patterns such as (0,0,1,1,2,2) ↦ 4 and several −2 slots).
The full identity is the universal quantification over all $4^6$ index tuples; individual chunk theorems pin single concrete points so the assembler can discharge them by case split.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin-4 literals are substituted into the fold definition of the numerator and the pattern table for the explicit kernel, so the equality is a pure integer decision.
why it matters
Feeds the parent assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; N=8Z$ and proves it by exhaustive fin_cases on all six indices, invoking one chunk theorem per cell. That universal identity is the algebraic core of the Regge exact-midpoint M2–TT certification in the Gravity analysis stack: it replaces a folded coupling sum by a sparse closed form, enabling exact (not approximate) midpoint identities in 4D discrete gravity. Within Recognition Science this sits in the gravity/Regge layer that must stay consistent with the forced $D=3$ spatial skeleton and the eight-tick discrete time structure; the chunk itself is pure integer bookkeeping, not a new physical postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.