e_022202
plain-language theorem explainer
Pointwise identity: the folded m2 numerator at multi-index (0,2,2,2,0,2) equals eight times the explicit Z table entry there. Gravity analysts assembling the full 4D Regge midpoint m2=8Z kernel cite this as one of 256 decide-chunks. Proof is a single kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,2,0,2)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer table $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2$ is defined by folding a fixed coupling list and summing a local contribution at each tuple. The companion table $Z$ is an explicit pattern-matched function returning small integers (e.g. $4$, $-2$) on selected index patterns and (implicitly) zero elsewhere.
The module is chunk 2 of a 256-way split of the identity $m_2=8Z$. Each chunk discharges one concrete multi-index by computation rather than by a structural argument, so the full forall can later be reassembled by exhaustive fin_cases.
Upstream, only the definitions of $m_2$ and $Z$ are required; no analytic lemma about curvature or edge lengths enters this line.
proof idea
One-line proof: by decide. Lean evaluates both sides at the fixed indices $(0,2,2,2,0,2)$ in the integer kernel and checks equality. No lemmas are invoked beyond the reducible definitions of the fold for $m_2$ and the pattern match for $Z$.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2=8Z$ and proves it by six nested fin_cases over $\mathrm{Fin},4$, hitting this chunk among the 256. That global identity is a certified algebraic step in the Regge-exact midpoint $M_2$ TT analysis for 4D gravity in the Recognition stack: it replaces a symbolic sum by a sparse explicit table, enabling later closed-form checks of the midpoint curvature kernel. It is bookkeeping inside the gravity analysis layer, not a forcing-chain (T0–T8) step, but it hardens the discrete geometric side that those continuum claims eventually rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.