e_011000
plain-language theorem explainer
For the single multi-index (0,1,1,0,0,0) on Fin 4, the folded M₂ numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it when assembling the full pointwise identity over all 4⁶ index sextuples. The proof is a one-shot `decide` on concrete integers.
Claim. For indices $a=0$, $b=1$, $c=1$, $d=0$, $i=0$, $j=0$ in $\mathrm{Fin}\,4$, the folded $M_2$ numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(0,1,1,0,0,0)=8\,Z_{\mathrm{expl}}(0,1,1,0,0,0)$.
background
The ambient module is a chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local claim is the pointwise relation $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ on one of 256 kernel cells (module doc: "m2Num = 8·explicitZ, chunk 1").
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those six Fin-4 indices. The explicit kernel $Z_{\mathrm{expl}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern of integer cases (values such as $4$, $-2$, and so on on distinguished index patterns).
Both objects live in the kernel-certificate module imported by this file; the present theorem only evaluates them at one concrete sextuple.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the fixed indices $(0,1,1,0,0,0)$ to concrete integers (the fold for the numerator versus the matching case of the explicit kernel) and checks equality by the decision procedure. No lemmas are invoked beyond the definitions of the two sides.
why it matters
This cell is one leaf of the exhaustive case split that builds the global identity. Downstream, m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by nested fin_cases on all six indices; each leaf discharges to a chunk theorem of this form.
In the Recognition gravity stack the identity is part of the exact midpoint analysis of the 4D Regge $M_2$ TT coupling. It is pure integer bookkeeping on Fin 4, not a continuum GR statement, and it does not itself invoke the forcing chain (T0–T8), RCL, or $\varphi$-ladder mass formulae. Its role is to close one certified cell so the assembler can finish the universal equality without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.