e_033003
plain-language theorem explainer
For the fixed six-index tuple (0,3,3,0,0,3) in Fin 4, the folded coupling numerator equals eight times the explicit integer table value. Gravity analysts cite it when discharging one cell of the 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $a{=}0$, $b{=}3$, $c{=}3$, $d{=}0$, $i{=}0$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $\sum_t \mathrm{contrib}(t;a,b,c,d,i,j)$ equals $8$ times the explicit integer value $Z(a,b,c,d,i,j)$ from the closed-form table.
background
This module is chunk 3 of a 256-cell kernel certification that the 4D Regge midpoint coupling numerator agrees with an explicit integer table, pointwise on $\mathrm{Fin},4^6$. The local claim is the scalar identity numerator $= 8\cdot Z$ at one fixed multi-index.
The numerator m2Num is defined by folding contrib over couplingZList, accumulating an Int. The comparison value explicitZ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite case table (e.g. $(0,0,1,1,2,2)\mapsto 4$, off-diagonal sign patterns $\mapsto -2$, and so on). Both live in the kernel certificate module imported here.
The theoretical setting is discrete gravity analysis: exact midpoint identities for the M2–TT sector in four dimensions, reduced to integer equalities that Lean can decide.
proof idea
One-line proof by decide. Both sides are closed integer terms once the six Fin 4 arguments are literals: the left side evaluates the fold of contrib over the fixed coupling list; the right side is eight times a single match arm of explicitZ. The kernel reduces both to numerals and checks equality. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the full pointwise identity $\forall a,b,c,d,i,j,; \mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one concrete cell so the assemble proof stays a pure case split rather than a large monolithic decide.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact midpoint M2–TT identity in 4D Regge calculus, not a forcing-chain landmark (T5–T8) or an RCL step. It closes one of 256 kernel obligations that underwrite the discrete curvature coupling used downstream in the gravity analysis modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.