e_122003
plain-language theorem explainer
At multi-index (1,2,2,0,0,3) the Regge midpoint coupling numerator equals eight times the explicit integer kernel. Gravity analysts proving the 4D M2TT midpoint identity cite this as one atomic kernel equality. The proof is a single decidability check on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,2,0,0,3)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(1,2,2,0,0,3)=8\,Z_{\mathrm{expl}}(1,2,2,0,0,3)$.
background
This module is chunk 6 of a 256-case kernel certification that the Regge-exact midpoint numerator equals eight times an explicit integer table on $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: it sums a local contribution at each table entry. The comparison target $Z_{\mathrm{expl}}$ is a hand-written integer function on six $\mathrm{Fin},4$ indices (sample clauses include $Z_{\mathrm{expl}}(0,0,1,1,2,2)=4$ and several $-2$ off-diagonal patterns).
The local claim is one pointwise instance of $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$, matching the module slogan "m2Num = 8·explicitZ, chunk 6 (256 kernel decides)."
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(1,2,2,0,0,3)$ and closes integer equality. No lemmas are invoked beyond the evaluability of the fold defining the numerator and the case table defining the explicit kernel.
why it matters
Feeds the assembled identity m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and is proved by exhaustive fin_cases on the six indices. That global equality is the certified numerator half of the Regge-exact midpoint M2TT identity in 4D gravity analysis inside the monolith.
Within Recognition Science gravity work, such kernel identities lock discrete curvature bookkeeping before continuum or phenomenological limits are taken. This declaration is pure scaffolding glue: one of 256 point checks, not a physical law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.