e_312130
plain-language theorem explainer
Pointwise identity: the Regge midpoint mass-squared numerator at the Fin-4 sextuple (3,1,2,1,3,0) equals eight times the explicit kernel Z there. Gravity analysts cite it as one cell of the 4D midpoint M2=8Z table. The proof is a single kernel decide on the unfolded integer equality.
Claim. For the index sextuple $(a,b,c,d,i,j)=(3,1,2,1,3,0)$ in $(\mathrm{Fin}\,4)^6$, the folded mass-squared numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a finite case table for the 4D Regge exact-midpoint identity equating the mass-squared numerator to eight times an explicit kernel. Indices run over $\mathrm{Fin},4$, so there are $4^6$ sextuples; they are partitioned into decide-chunks.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a coupling list and summing a local contribution at each tuple. The explicit kernel $Z$ is a closed integer-valued pattern on the same six indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$). The claim is pure integer arithmetic after those definitions unfold.
Local setting (module doc): prove $m_2^{\mathrm{num}}=8\cdot Z$ cellwise via kernel decides, then assemble.
proof idea
One-line computational proof: decide. Lean unfolds m2Num (the fold over couplingZList of contrib) and explicitZ at the concrete sextuple $(3,1,2,1,3,0)$, reduces both sides to closed integers, and checks equality. No lemmas beyond the two upstream defs; no induction or algebraic rewrite.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges the universal quantifier by fin_cases on all six indices. Each concrete cell such as this one is a leaf of that case tree.
In the gravity analysis stack this is bookkeeping for the 4D Regge midpoint mass-squared / TT-identity kernel: once every cell matches, the numerator is identically eight times the explicit $Z$ pattern. That identity is infrastructure for the broader Regge-exact midpoint certification, not a forcing-chain (T0–T8) step. No open scaffold remains at this leaf; the open work sits at assembly and at using the assembled identity downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.