e_112002
plain-language theorem explainer
Concrete kernel identity: the midpoint M2 numerator at multi-index (1,1,2,0,0,2) equals eight times the explicit Z-table entry. Gravity analysts cite it when assembling the full 4D Regge midpoint M2=8Z identity. The proof is a single kernel decide on the two integer sides.
Claim. For indices $(a,b,c,d,i,j)=(1,1,2,0,0,2)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 5 of a 256-case kernel certification that the 4D Regge midpoint M2 numerator equals eight times an explicit integer table. The ambient setting is discrete gravity analysis: exact midpoint identities for the TT sector of the Regge action in four dimensions.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six $\mathbb{F}_4$ indices. The table $Z$ is a pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and other small integers on the listed patterns).
The local claim is one coordinate of the global equality $m_2^{\mathrm{num}}=8Z$, restricted to the multi-index $(1,1,2,0,0,2)$.
proof idea
One-line kernel proof: both sides reduce to concrete integers once the six Fin-4 arguments are fixed, so decide discharges the equality. No algebraic lemmas are invoked beyond the definitions of the folded numerator and the explicit table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathbb{F}_4)^6$ by exhausting cases. That global equality is the certified algebraic core of the 4D Regge exact-midpoint M2/TT analysis in this gravity stack.
Within Recognition Science gravity work, such kernel chunks close the discrete curvature bookkeeping that later couples to continuum limits and continuum constants. The chunk does not itself touch the forcing chain (T5 J-cost, T6 $\varphi$, T7 eight-tick, T8 $D=3$); it is infrastructure under the Regge side of the gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.