e_321302
plain-language theorem explainer
Pointwise kernel identity: for indices (3,2,1,3,0,2) the midpoint m₂ numerator equals eight times the explicit Z table entry. Gravity analysts cite it when assembling the full Fin-4^6 identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a=3$, $b=2$, $c=1$, $d=3$, $i=0$, $j=2$ in $\{0,1,2,3\}$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M₂ TT identity certification. The local claim family is $m_2^{\mathrm{num}}=8\cdot Z$ on six Fin-4 indices, discharged by kernel decides.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: each term contributes an integer via a local contrib map, and the fold starts at 0. The comparison target explicitZ is a closed integer table on the same six indices (sample entries include $4$, $-2$, and other small integers on the diagonal and off-diagonal patterns).
Upstream, both definitions live in the KernelCert module; this chunk only evaluates one concrete sextuple against that shared table and fold.
proof idea
One-line computational proof: decide. After the six Fin-4 arguments are substituted, both sides reduce to concrete integers (the fold of contrib versus eight times the matching explicitZ clause), and the decision procedure checks equality.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathrm{Fin},4$, $m_2^{\mathrm{num}}=8\cdot Z$, by exhaustive fin_cases on all six indices. Each chunk theorem such as this one closes one generated goal in that case split (module doc: chunk 14 of the 256 kernel decides).
In the broader Gravity analysis, the identity is part of certifying the exact midpoint M₂ TT structure used in the Regge-side discrete curvature bookkeeping. It is pure integer algebra on the coupling kernel, not a continuum GR derivation, and sits downstream of the KernelCert table definitions rather than of the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.