e_203300
plain-language theorem explainer
For multi-index (2,0,3,3,0,0), the folded midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one of the 256 Fin-4 kernel cases that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(2,0,3,3,0,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of the 4D Regge exact-midpoint M2TT identity certification: each chunk discharges a block of the 256 kernel equalities $m_2^{\mathrm{num}}=8\cdot Z$ by direct decision.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each term's contribution at the six Fin-4 indices. The comparison target explicitZ is a closed-form integer table on $(\mathrm{Fin},4)^6$ (sample entries include $4$ on diagonal-like pairs and $-2$ on crossed pairs).
The local setting is pure integer kernel arithmetic inside the gravity analysis stack; no continuum limit or variational argument is invoked at this layer.
proof idea
One-line proof: by decide. Lean evaluates both sides of the equality at the concrete indices $(2,0,3,3,0,0)$ (folding the coupling list on the left, looking up the explicit table on the right) and accepts the integer identity. No lemmas beyond the two definitions are required.
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\cdot Z$ and proves it by exhaustive fin_cases over all six Fin-4 indices, dispatching each cell to a chunk equality of this form.
In the Recognition gravity stack these kernel identities underwrite the exact midpoint mass-squared / TT structure used in the discrete Regge analysis. They are bookkeeping, not a forcing-chain step (T0–T8), but they close a finite certificate that downstream continuum or continuum-limit arguments can treat as discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.