e_210213
plain-language theorem explainer
One of 256 kernel equalities certifying that the folded numerator m2Num equals eight times the closed-form table explicitZ, here at index tuple (2,1,0,2,1,3). Gravity analysts assembling the 4D Regge midpoint M2TT identity cite the full forall; this chunk entry is a single decide cell. Proof is pure kernel evaluation of both sides as integers.
Claim. For the six indices $(a,b,c,d,i,j)=(2,1,0,2,1,3)$ in $\mathrm{Fin}\,4$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8$ times the explicit table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the M2TT identity is reduced to an integer identity between two functions of six $\mathrm{Fin},4$ indices. The numerator side $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the given indices. The comparison side is an explicit piecewise table $Z$ on those six indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The local module is chunk 9 of a 256-cell decide grid that exhausts every index combination. The module claim is the pointwise relation $m_2^{\mathrm{num}}=8\cdot Z$. The full quantified statement is assembled downstream by nested fin_cases over all six arguments.
proof idea
One-line decide. Both sides are closed integer expressions once the six concrete Fin 4 values are substituted: the fold that defines $m_2^{\mathrm{num}}$ evaluates to a numeral, the matching clause (or default) of the explicit table $Z$ evaluates to a numeral, and the kernel checks $n=8\cdot z$ by computation. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges the universal quantifier by fin_cases on each coordinate, hitting this cell among the 256. That global equality is the algebraic backbone of the Regge exact midpoint M2TT identity certification in 4D gravity analysis inside the monolith. It is bookkeeping, not a new physical law: once every chunk cell holds, the midpoint discrete curvature identity is an integer fact rather than a symbolic obligation. No T0–T8 forcing step is touched directly; the result sits in the gravity analysis layer that consumes the already-forced $D=3$ spatial setting and the discrete tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.