e_022322
plain-language theorem explainer
For the six-index slot (0,2,2,3,2,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over the 4D midpoint Regge kernel. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}2$, $d{=}3$, $i{=}2$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,2,2,3,2,2)=8\,Z(0,2,2,3,2,2)$.
background
This module is one chunk of the 4D midpoint Regge identity that asserts the folded numerator equals eight times an explicit integer table. The local setting is stated as "m2Num = 8·explicitZ, chunk 2 (256 kernel decides)": the full six-index space $(\mathrm{Fin},4)^6$ is partitioned into decide-sized pieces.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a contribution at each term. The explicit kernel $Z$ is a pattern-matched integer table on six $\mathrm{Fin},4$ indices (sample values include $4$, $-2$, and so on). Both live in the kernel certificate module imported here.
The present declaration fixes one concrete six-tuple and checks the scalar identity at that point, feeding the exhaustive case split that rebuilds the universal statement.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold that defines the numerator at $(0,2,2,3,2,2)$, the right-hand side multiplies the table lookup of the explicit kernel by eight. No lemmas beyond the definitions of the numerator and the explicit kernel are required; the kernel closes the equality.
why it matters
This is one atomic cell in the assembly of m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by nested fin_cases over all six indices. Downstream, that universal identity is the certified algebraic core of the exact midpoint $M_2$ TT identity in 4D Regge gravity analysis inside the monolith.
In the Recognition Science gravity stack, such kernel identities underwrite discrete curvature and mass-response bookkeeping on the phi-ladder side of the continuum limit. The chunking strategy (256 decides per chunk) keeps each certificate small while still discharging the full finite case space without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.