e_302033
plain-language theorem explainer
For the six-index tuple (3,0,2,0,3,3) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one cell of the 256-point kernel that certifies the Regge exact-midpoint M2TT identity in 4D. The proof is a single decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}0$, $c{=}2$, $d{=}0$, $i{=}3$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
This module is one chunk of the 256 kernel decides that establish the pointwise identity m2Num = 8·explicitZ on Fin 4^6. The ambient setting is the Regge exact-midpoint analysis of the 4D M2TT gravitational identity: discrete curvature couplings are reduced to integer arithmetic on six Fin-4 indices.
The numerator m2Num(a,b,c,d,i,j) is defined by folding a fixed coupling list and summing a local contribution at each term. The comparison value explicitZ is a sparse closed-form table on the same six indices (nonzero only on a short list of patterns such as (0,0,1,1,2,2) ↦ 4 and (0,0,1,2,1,2) ↦ −2).
The full universal statement is assembled downstream by exhausting all Fin-4 cases; each chunk theorem such as this one discharges a single concrete sextuple.
proof idea
One-line kernel decide. Both sides evaluate to concrete integers once the six Fin-4 arguments are fixed to (3,0,2,0,3,3): m2Num reduces by folding the coupling list, explicitZ by table lookup (or default). Lean’s decide closes the resulting integer equality with no lemmas beyond the two definitions.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states ∀ a b c d i j, m2Num = 8 · explicitZ and is proved by nested fin_cases that invoke one decide per cell. That universal equality is the algebraic core of the Regge exact-midpoint M2TT identity in 4D gravity analysis inside the monolith.
In the broader Recognition Science gravity stack, certifying the discrete midpoint kernel supports the continuum limit and the dimensional forcing (T8: D = 3 spatial) once the lattice couplings are matched. This declaration is pure scaffolding glue: one of 256 identical cells, not a conceptual step by itself, but required for the assembler to be sorry-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.