e_022031
plain-language theorem explainer
For the six-index slot (0,2,2,0,3,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these micro-identities when assembling the global Regge midpoint M2=8Z relation in 4D. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}2$, $d{=}0$, $i{=}3$, $j{=}1$ 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 one chunk of the 4D Regge exact-midpoint certification that the folded numerator $m_2^{\mathrm{num}}$ equals eight times a sparse explicit integer kernel $Z$. The module header states the goal bluntly: $m_2^{\mathrm{num}}=8\cdot Z$, chunk 2, discharged by 256 kernel decides.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing local contributions at those six Fin-4 indices. The companion $Z$ is an explicit pattern-matched integer table on the same six indices (typical nonzero entries are $\pm 2$ or $4$). Both live in the kernel-cert module imported here.
The present declaration fixes one concrete sextuple $(0,2,2,0,3,1)$ inside that table. Sibling theorems cover the other index combinations in the same chunk.
proof idea
One-line proof by decide. Lean evaluates both sides at the concrete Fin-4 indices: the left-hand fold of coupling contributions and the right-hand $8\cdot Z$ lookup reduce to equal integers in Int, so the kernel closes the equality with no further lemmas.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases over all six indices and dispatch to these chunk identities. That global identity is the algebraic core of the Regge exact-midpoint $M_2$ certification in 4D gravity analysis inside the monolith.
In the broader Recognition Science gravity stack, such exact discrete identities underwrite curvature and mass-ladder bookkeeping on the eight-tick / $D=3$ side; they are computational certificates rather than new physical postulates. No open scaffold remains on this slot once decide succeeds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.