e_123022
plain-language theorem explainer
For the six Fin-4 indices (1,2,3,0,2,2), the folded numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts assembling the 4D Regge midpoint M2 identity cite this as one of the 256 kernel point checks. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}1,b{=}2,c{=}3,d{=}0,i{=}2,j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value at those indices.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices appear. The numerator $\mathrm{m2Num}$ is defined by folding a fixed coupling list: it sums a contribution function over that list and returns an $\mathrm{Int}$. The companion $\mathrm{explicitZ}$ is a closed pattern-match table that assigns small integers (e.g. $4$, $-2$, and so on) to particular index sextuples.
The local module is chunk 6 of a 256-point kernel certification that $\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ at every index. Each chunk theorem pins one concrete sextuple so the assembler can discharge the universal statement by exhaustive $\mathrm{fin_cases}$.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted into the fold definition of m2Num and the pattern-match table explicitZ, so the equality is a pure integer decision.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,;\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ and proves it by nested fin_cases over all six indices. That universal identity is the algebraic backbone of the exact midpoint M2 TT identity in the 4D Regge gravity analysis. Without the per-point chunk equalities, the fin_cases tree would have nothing to close on. This is pure discrete certification inside the gravity domain, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.