e_010300
plain-language theorem explainer
For the six-index tuple (0,1,0,3,0,0) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel entry. Gravity analysts cite it as one cell of the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(0,1,0,3,0,0)$ equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(0,1,0,3,0,0)=8\,Z_{\mathrm{ex}}(0,1,0,3,0,0)$.
background
This module is chunk 1 of a 256-cell kernel certification that the 4D Regge midpoint numerator $m_2^{\mathrm{num}}$ agrees with eight times a closed-form integer table $Z_{\mathrm{ex}}$. Both maps take six arguments in $\mathrm{Fin},4$ (two edge pairs and a midpoint pair) and return an Int.
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing each term's contribution at the six indices. $Z_{\mathrm{ex}}$ is an explicit pattern-match table (e.g. $(0,0,1,1,2,2)\mapsto 4$, mixed pairs $\mapsto -2$). The local claim is only the equality at one concrete multi-index.
The ambient goal is an exact algebraic identity for the midpoint M2TT kernel in discrete gravity, not a continuum limit statement.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left by evaluating the fold of couplingZList contributions at $(0,1,0,3,0,0)$, the right by looking up explicitZ and multiplying by 8. The kernel checks integer equality; no lemmas are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ and discharges the universal claim by fin_cases on all six indices, invoking one cell theorem per tuple. This chunk is one of those cells.
In the Recognition gravity stack, the identity certifies that the discrete midpoint curvature/coupling numerator matches the explicit 4D kernel used in Regge-type analyses. It is pure finite combinatorics on $\mathrm{Fin},4$; it does not itself invoke the forcing chain (T0–T8), $\varphi$, or continuum Einstein equations, but it underwrites the exact discrete side of those gravity comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.