e_000002
plain-language theorem explainer
Pointwise identity: the midpoint mass-squared numerator at multi-index (0,0,0,0,0,2) equals eight times the explicit kernel value at that same index. Gravity analysts cite it when assembling the full 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,0,0,0,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel entry $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is obtained by folding a fixed coupling list: each term contributes an integer depending on six $\mathrm{Fin},4$ indices, and the fold starts from zero. The companion map $Z$ is an explicit piecewise integer table on the same six-index domain (values such as $4$, $-2$, and so on on the listed patterns, and implicitly zero elsewhere in the certified kernel).
The local module is chunk 0 of a 256-way kernel split: each chunk discharges a block of concrete index tuples so that the global identity $m_2^{\mathrm{num}}=8Z$ can be reassembled by exhaustive fin_cases. The present tuple is one cell in that grid.
proof idea
One-line decide proof. Both sides reduce to concrete integers once the six indices are fixed: the fold that defines the numerator evaluates to a single Int, the explicit table returns a single Int, and Lean’s kernel checks the equality $n=8z$ by computation. No lemmas are invoked beyond the two definitions.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by casing on each coordinate and invoking the chunk theorems. That global equality is the algebraic core of the Regge exact midpoint M2–TT identity in 4D gravity analysis inside the monolith. It sits in the Gravity domain rather than the T0–T8 forcing chain, but it is the kind of fully discharged integer identity the framework needs before continuum or continuum-limit claims can be attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.