e_032132
plain-language theorem explainer
For the six-index slot (0,3,2,1,3,2) on Fin 4, the folded Regge coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it as one cell of the 4D midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(0,3,2,1,3,2)$. Writing $N$ for the fold of coupling contributions over the fixed coupling list and $Z$ for the explicit integer kernel on the same indices, one has $N(0,3,2,1,3,2)=8\,Z(0,3,2,1,3,2)$.
background
The ambient module is a chunk of the 4D Regge exact-midpoint M2–TT identity: the claim that the folded numerator m2Num equals eight times a closed-form integer table explicitZ on every six-tuple of Fin-4 indices. The module doc states the local goal as "m2Num = 8·explicitZ, chunk 3 (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 (sample clauses include values 4, −2, and so on). Both live in the KernelCert import; this file only discharges concrete equalities.
Chunk theorems such as this one cover individual index cells so a later assembler can reassemble the universal statement by fin_cases.
proof idea
One-line computational proof: by decide. Lean reduces both sides on the concrete Fin-4 sextuple (0,3,2,1,3,2) to integers and checks equality in the kernel. No lemmas are invoked beyond the definitions of the numerator fold and the explicit kernel table.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states ∀ six Fin-4 indices, the numerator equals eight times the explicit kernel, proved by exhaustive fin_cases that routes each cell to a chunk equality of this form. Without the cell facts, the universal midpoint identity does not close.
In the Recognition gravity stack this is bookkeeping for the 4D Regge/TT side of the exact-midpoint analysis, not a forcing-chain (T0–T8) step. It is pure finite enumeration supporting a certified algebraic identity used downstream in the gravity analysis modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.