e_310012
plain-language theorem explainer
For the six-index tuple (3,1,0,0,1,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 all 4^6 index patterns. The proof is a pure kernel decide on concrete integers.
Claim. For indices $a=3$, $b=1$, $c=0$, $d=0$, $i=1$, $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
In the Regge exact-midpoint 4D analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start from 0 and add each contribution term at the six Fin-4 indices. The companion map explicitZ is a sparse integer table on those same six indices (typical nonzero values $\pm 2,4$ on selected patterns).
This module is chunk 13 of a 256-way kernel split that discharges $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The local setting is pure integer arithmetic on Fin 4; no continuum limit or physical units enter the statement.
Upstream, m2Num and explicitZ are the two sides being compared. The full quantified identity is assembled later by exhaustive fin_cases over all six indices.
proof idea
One-line kernel proof: decide evaluates both sides at the concrete indices (3,1,0,0,1,2) and checks integer equality. No lemmas are invoked beyond the definitions of m2Num (fold of contrib over couplingZList) and explicitZ (pattern-match table).
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ by fin_cases on each coordinate and dispatch to these chunk equalities. That global identity is the algebraic certificate that the midpoint Regge $M_2$ TT numerator matches eight times the closed-form kernel in 4D.
Within Recognition gravity analysis this is bookkeeping, not a new physical law: it closes one cell of the 256-decide grid so the assembled equality can be cited without residual case obligations. It does not itself touch the forcing chain (T0–T8), RCL, or the phi-ladder mass formula; those enter only if a later gravity bridge uses the certified $M_2$ identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.