e_222003
plain-language theorem explainer
For the six-index cell (2,2,2,0,0,3), the midpoint mass-squared numerator equals eight times the explicit kernel integer. Gravity analysts assembling the 4D Regge exact midpoint M2TT identity cite it as one decided cell in chunk 10. The proof is a single kernel `decide` on concrete integers.
Claim. With six indices in $\{0,1,2,3\}$, the folded numerator $m_2^{\mathrm{num}}(2,2,2,0,0,3)$ equals $8$ times the explicit kernel value $Z(2,2,2,0,0,3)$.
background
In the 4D Regge exact-midpoint analysis, two integer tables on six Fin 4 indices are compared. The numerator m2Num a b c d i j is the fold of contrib over couplingZList, summing coupling contributions at those indices. The companion explicitZ is a piecewise integer kernel (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
This module is chunk 10 of the cell-by-cell certification that the numerator is identically eight times the explicit kernel. The module doc states the goal directly: m2Num = 8·explicitZ, discharged by 256 kernel decides per chunk. Sibling lemmas cover the neighboring index tuples in the same block.
proof idea
One-line proof: by decide. Both sides reduce to concrete Int values at the fixed indices $(2,2,2,0,0,3)$, so the kernel closes the equality with no lemmas or rewriting.
why it matters
Parent theorem m2Num_eq_eight_explicitZ asserts the identity for every six-tuple of Fin 4 indices, by exhaustive fin_cases on each coordinate. This cell lemma is one of the concrete discharges that assembly depends on.
In the gravity stack, the identity ties the folded coupling numerator to the closed-form kernel used in the Regge exact-midpoint M2TT analysis in four dimensions. It is bookkeeping infrastructure rather than a forcing-chain step (T0–T8), but without the cell equalities the global numerator–kernel match cannot be certified in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.