e_112202
plain-language theorem explainer
For the Fin-4 multi-index (1,1,2,2,0,2), the folded coupling numerator equals eight times the closed-form kernel integer. Gravity analysts certifying the exact midpoint M2 TT identity in 4D Regge calculus cite this as one concrete kernel case among 4^6. The proof is a single decide evaluation of both integer sides.
Claim. For indices $a=1$, $b=1$, $c=2$, $d=2$, $i=0$, $j=2$ in $\mathrm{Fin}\,4$, the summed coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(1,1,2,2,0,2)=8\,Z(1,1,2,2,0,2)$.
background
In the 4D Regge midpoint analysis, the numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is an integer obtained by folding a fixed coupling list and summing local contributions at each multi-index in $(\mathrm{Fin},4)^6$. The companion map $Z$ (explicitZ) is a sparse integer table on the same domain, recording closed-form kernel entries such as $4$ or $-2$ at selected index patterns.
This module is chunk 5 of the exhaustive check that the numerator equals eight times the explicit kernel at every multi-index. The parent kernel-certificate module supplies both definitions; the present file discharges a block of decide goals (256 per the module header) inside the full $4^6=4096$ case grid.
The local setting is pure finite integer identity: no continuum limit or physical units enter the statement.
proof idea
One-line proof by decide. With all six arguments concrete Fin 4 literals, both sides reduce to closed integer expressions: the fold that defines the numerator, and eight times the pattern-matched kernel table. The kernel evaluates both sides and accepts the equality. No intermediate lemmas are invoked beyond the two definitions.
why it matters
This case feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases. That global equality is the certified numerator form of the exact midpoint M2 TT identity in 4D Regge calculus.
Inside the Recognition gravity stack, such kernel identities underwrite discrete curvature bookkeeping that links Regge calculus to continuum structure. The entry is one parallel decide certificate among many sibling chunks; together they close the finite case analysis with no sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.