e_213331
plain-language theorem explainer
Kernel certificate that the midpoint Regge m2 numerator at multi-index (2,1,3,3,3,1) equals eight times the explicit Z table entry. Gravity analysts assembling the 4D midpoint TT identity cite these 256 index chunks. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,3,3,3,1)$ 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 table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 9 of a 256-way kernel split proving $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathrm{Fin},4)^6$. The setting is the exact midpoint identity for the 4D Regge TT sector in the Gravity.Analysis stack.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each local contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison table $Z$ is an explicit six-argument integer function on $\mathrm{Fin},4$, given by a finite pattern of nonzero entries (e.g. $4$, $-2$) and zero elsewhere.
Both definitions live in the KernelCert module imported here. The full quantified identity is assembled downstream by exhausting all index sextuples.
proof idea
One-line computational proof: by decide. After substituting the concrete Fin-4 indices $(2,1,3,3,3,1)$, both sides reduce to closed integer expressions (the fold for $m_2^{\mathrm{num}}$ versus $8$ times the matching $Z$ clause), and Lean's decision procedure checks equality.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges the claim by fin_cases on each coordinate, invoking one chunk per residue class. Without these pointwise certificates the midpoint Regge TT identity in 4D has no certified numerator reduction. The factor $8$ is the combinatorial normalization tying the folded coupling sum to the sparse explicit table used in the broader gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.