e_201012
plain-language theorem explainer
For the six-index tuple (2,0,1,0,1,2) in (Fin 4)^6, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic case in the 256-way kernel certification of the Regge midpoint M2 TT identity. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,0,1,2)$ with each entry in $\{0,1,2,3\}$, the integer numerator $m_2^{\mathrm{num}}(2,0,1,0,1,2)$ obtained by folding coupling contributions equals $8\,Z(2,0,1,0,1,2)$, where $Z$ is the explicit piecewise kernel on $(\mathrm{Fin}\,4)^6$.
background
In the 4D Regge exact-midpoint analysis, the TT-sector mass-squared numerator is assembled by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums contrib over couplingZList. The companion explicitZ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite pattern match (typical values $\pm 2,\pm 4$, else zero).
The module certifies the identity $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. With six indices in a four-element type there are $4^6=4096$ formal slots, but the kernel is sparse; this file is chunk 8 of the decide-driven cases that pin the nonzero (and selected zero) cells.
Upstream, explicitZ and m2Num are pure definitions in the KernelCert module; no analytic lemma is required beyond evaluating those defs at a concrete hex-tuple.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the closed indices $(2,0,1,0,1,2)$ to concrete integers (left via the fold definition of m2Num, right via the pattern match of explicitZ) and checks equality in Int. No lemmas are invoked beyond the two defs.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and is proved by exhaustive fin_cases on all six indices, dispatching each cell to a chunk theorem such as this one.
That global identity is the algebraic core of the Regge exact-midpoint M2 TT certification in 4D: it replaces the folded coupling sum by an explicit sparse kernel, enabling closed-form checks of the TT mass-squared structure in the gravity analysis stack. It is bookkeeping inside the discrete curvature/Regge sector rather than a forcing-chain (T0–T8) step, but it is load-bearing for the exact midpoint identities used downstream in the RS gravity pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.