e_320302
plain-language theorem explainer
For the six Fin-4 indices (3,2,0,3,0,2), the midpoint Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the 4D TT midpoint identity cite this as one of the 256 kernel cells. The proof is a pure decide on the concrete integer equality.
Claim. For indices $a=3$, $b=2$, $c=0$, $d=3$, $i=0$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 14 of a 256-cell kernel certification that the midpoint Regge numerator equals eight times a closed-form integer table. The ambient setting is 4D discrete gravity analysis: six indices each run over $\mathrm{Fin},4$, labeling edge/face slots in the TT midpoint identity.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on the six indices (typical nonzero values $\pm 2,\pm 4$ on diagonal and off-diagonal pairings).
The global claim is pointwise equality $m_2^{\mathrm{num}}=8,Z$ on every cell. Each chunk theorem discharges one concrete sextuple so the assembler can finish by exhaustive fin_cases.
proof idea
One-line computational proof: decide evaluates both sides of the integer equality at the fixed indices $(3,2,0,3,0,2)$ and checks they match. No lemmas are invoked beyond the definitions of the folded numerator and the explicit kernel table; the kernel is small enough that Lean’s decision procedure closes the cell directly.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z$ and proves it by six nested fin_cases over $\mathrm{Fin},4$, dispatching each leaf to a chunk identity of this form. Without the full 256-cell cover, the midpoint TT numerator identity in 4D Regge analysis stays open.
In the Recognition gravity stack this is pure discrete-kernel bookkeeping: it certifies that the combinatorial numerator matches the closed-form $Z$ table used downstream in curvature and mass-gap arguments. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is infrastructure for the Regge exact-midpoint layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.