e_211311
plain-language theorem explainer
One of 256 concrete kernel equalities: the midpoint mass-squared numerator at multi-index (2,1,1,3,1,1) equals eight times the explicit Z-table entry. Gravity analysts cite it only as a discharged case inside the assembled identity m2Num = 8·explicitZ on (Fin 4)^6. The proof is a single kernel decide on fixed integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,1,1,3,1,1)$ with each coordinate in $\{0,1,2,3\}$, 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 case split proving $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on six indices in $\mathrm{Fin},4$. The setting is the exact midpoint mass-squared identity for 4D Regge calculus in the Recognition gravity stack.
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 indices. The comparison table $Z$ is an explicit piecewise integer function on $(\mathrm{Fin},4)^6$ (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both objects live in the kernel certificate module; the chunk files only pin individual sextuples so the assembler can recombine them without a monolithic decide.
proof idea
One-line computational proof: decide. After the six concrete Fin 4 arguments are substituted, both sides reduce to closed integer expressions (a finite fold versus a table lookup), and the kernel decision procedure checks equality. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases. That universal equality is the algebraic core of the exact midpoint $M_2$ TT identity in 4D Regge analysis: it certifies that the folded coupling numerator is exactly eight copies of the closed-form $Z$ table, with no residual terms.
Within Recognition gravity this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8). It closes one of the 256 kernel obligations so the assembled identity can be cited downstream without sorry. Open scaffolding elsewhere in the gravity stack is unaffected; this chunk only discharges its own index.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.