e_331101
plain-language theorem explainer
One kernel cell of the 4D Regge midpoint identity: the folded numerator m2Num at index tuple (3,3,1,1,0,1) equals eight times the closed-form table explicitZ at the same indices. Gravity analysts assembling the full m2Num = 8·explicitZ identity cite this cell. The proof is a pure decide on concrete integers.
Claim. For the six indices $(a,b,c,d,i,j)=(3,3,1,1,0,1)$ in $\mathrm{Fin}\,4$, the integer numerator obtained by folding the coupling list equals eight times the explicit closed-form table entry: $m_2^{\mathrm{num}}(3,3,1,1,0,1)=8\,Z_{\mathrm{expl}}(3,3,1,1,0,1)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each term. The companion map $Z_{\mathrm{expl}}$ is an explicit piecewise table of small integers (entries such as $4$, $-2$, and so on) that is meant to be the closed form of that fold, up to a universal factor of eight.
The ambient module is one of the decide-chunks that discharge the identity cell-by-cell: "m2Num = 8·explicitZ, chunk 15 (256 kernel decides)." Each chunk theorem fixes one concrete six-tuple and asserts equality of the two integers. Upstream, only the definitions of the fold and of the table are required; no analytic lemma is invoked.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete indices $(3,3,1,1,0,1)$ to ground integers (the fold over the coupling list on the left, the matching table clause on the right) and checks equality by the kernel decision procedure. No rewrite, induction, or named lemma is applied.
why it matters
This cell is consumed by the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ and proves it by exhaustive fin_cases on all six indices. Each case lands on one of the chunk theorems such as this one. The full identity is the algebraic backbone of the exact midpoint $M_2$ TT identity in the 4D Regge analysis used on the gravity side of the Recognition Science mirror. It does not itself touch the forcing chain (T5–T8) or the RCL; it is pure discrete tensor bookkeeping that keeps the continuum limit certificates honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.