e_102000
plain-language theorem explainer
Pointwise kernel identity: at multi-index (1,0,2,0,0,0), the folded numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of the 256 decide-chunks. The proof is a single kernel decision (`decide`).
Claim. For the multi-index $(a,b,c,d,i,j)=(1,0,2,0,0,0)\in(\mathrm{Fin}\,4)^6$, the integer numerator $m_2^{\mathrm{num}}(1,0,2,0,0,0)$ equals $8\,Z(1,0,2,0,0,0)$, where $Z$ is the explicit piecewise table and $m_2^{\mathrm{num}}$ is the fold of coupling contributions over the coupling list.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on $(\mathrm{Fin},4)^6$ are compared. The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: each term contributes an integer via a local contribution map, and the fold starts at $0$. The comparison target is an explicit piecewise table $Z$ on the same six indices, with sparse nonzero values such as $\pm 2,,4$ on selected patterns.
The local module is chunk 4 of a 256-way partition of the finite domain: the claim is the scalar identity $m_2^{\mathrm{num}}=8,Z$ at one fixed sextuple. Upstream, both $m_2^{\mathrm{num}}$ and $Z$ are pure definitions in the kernel certificate module; no analytic hypothesis is carried.
The ambient goal is an exact algebraic identity used in the discrete gravity / Regge calculus side of the Recognition stack, not a continuum limit statement.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete Fin-4 indices to closed integers (the fold for $m_2^{\mathrm{num}}$ and the matching clause or default of $Z$) and checks equality by the kernel decision procedure. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ and $Z$.
why it matters
This chunk is one leaf in the exhaustive case split that builds m2Num_eq_eight_explicitZ, the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$. That parent theorem proceeds by nested fin_cases on all six indices and dispatches each cell to a decide-chunk of this form.
In the gravity analysis layer, equating the folded coupling numerator to eight times the explicit table certifies the midpoint M2–TT kernel identity in 4D Regge calculus. The factor $8$ matches the eight-tick / $2^3$ octave bookkeeping familiar from the forcing chain (T7), though here it appears as a pure combinatorial coefficient on a finite index set. Closing all 256 cells removes scaffolding from the discrete curvature side of the RS gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.