e_110302
plain-language theorem explainer
For the six Fin-4 indices (1,1,0,3,0,2), the Regge midpoint numerator m2Num equals eight times the closed-form explicitZ value at those indices. Gravity analysts cite it when assembling the full pointwise identity m2Num = 8·explicitZ over the 4D kernel. The proof is a single kernel decide on concrete integers.
Claim. For $a=1$, $b=1$, $c=0$, $d=3$, $i=0$, $j=2$ in $\mathrm{Fin}\,4$, the midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer depending on six indices in $\mathrm{Fin},4$, and the fold starts from zero. The companion map explicitZ is a piecewise integer table on the same six indices (sample values include $4$, $-2$, and so on for distinguished patterns).
The module is chunk 5 of a 256-way kernel split whose sole job is to discharge $m_2^{\mathrm{num}}=8\cdot Z$ at concrete index tuples by decision procedure. Upstream, both $m_2^{\mathrm{num}}$ and explicitZ live in the kernel certificate module; this chunk only evaluates one ordered sextuple.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete Fin-4 values $(1,1,0,3,0,2)$ to bare integers and checks equality in the kernel. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (the fold) and explicitZ (the table).
why it matters
The parent theorem is the assembled identity: for all six indices in $\mathrm{Fin},4$, $m_2^{\mathrm{num}}=8\cdot Z$. That proof runs nested fin_cases over every coordinate and lands on chunk lemmas such as this one. Without the pointwise decides, the global midpoint numerator identity in the 4D Regge kernel would not close. The result is pure discrete gravity bookkeeping inside the Recognition gravity stack; it does not itself invoke the forcing chain (T5–T8) or the RCL, but it underwrites exact algebraic control of the midpoint mass-squared numerator used downstream in that stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.