e_302000
plain-language theorem explainer
For the single multi-index (3,0,2,0,0,0) on Fin 4, the folded m2 numerator equals eight times the explicit integer kernel value. Gravity analysts assembling the 4D Regge midpoint TT identity cite this as one of the 256 kernel cases. The proof is a pure `decide` discharge of that concrete integer equality.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(3,0,2,0,0,0)=8\,Z_{\mathrm{expl}}(3,0,2,0,0,0)$, where $Z_{\mathrm{expl}}$ is the explicit integer table and $m_2^{\mathrm{num}}$ is the fold of coupling contributions.
background
This module is one chunk of the 4D Regge exact-midpoint TT identity certification: it records that the folded numerator equals eight times an explicit integer kernel, case by case (256 kernel decides total; this file is chunk 12).
Upstream, m2Num is defined by folding contrib over couplingZList at a six-index slot $(a,b,c,d,i,j)\in(\mathrm{Fin},4)^6$, yielding an Int. The companion explicitZ is a pattern-matched integer table on the same index type (sample clauses send e.g. $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$). The local claim is the pointwise factor-of-eight match at one fixed tuple.
The surrounding analysis sits in the gravity stack that certifies an exact midpoint identity for the TT sector in four dimensions, reducing symbolic coupling sums to a finite kernel check.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the concrete indices $(3,0,2,0,0,0)$—the fold that defines the numerator on the left, and the pattern match that defines the explicit table on the right—and closes the resulting integer equality in the kernel. No lemmas are invoked beyond the two definitions.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ by exhausting all six Fin 4 indices. This declaration supplies one cell of that exhaustion (chunk 12 of the decide grid).
In the Recognition gravity analysis, the factor-of-eight match turns a folded coupling sum into a closed integer kernel, which is the algebraic content needed for the exact midpoint TT identity in 4D. It is bookkeeping, not a new physical law, but without the full 256-case cover the assemble theorem does not go through. No T0–T8 forcing step is discharged here; the link is downstream in the Regge/TT certification path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.