e_010131
plain-language theorem explainer
Pointwise identity: the Regge midpoint coupling numerator at index sextuple (0,1,0,1,3,1) equals eight times the explicit integer table entry. One of 256 kernel decides in chunk 1 that feed the universal assembly theorem over all Fin-4 indices. Proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,1,3,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
The module sits in the 4D Regge midpoint analysis of the $M_2$ TT kernel identity. The local goal, stated in the module header, is to certify $m_2^{\mathrm{num}}=8\cdot Z$ by a grid of 256 kernel decides (chunk 1).
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined as the fold of couplingZList, summing a contribution at each coupling term for the six $\mathrm{Fin},4$ indices. The companion table $Z$ is an explicit integer-valued function on the same six indices, with sparse nonzero cases (e.g. $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$).
Both objects live in the kernel certificate module; this chunk only evaluates them at fixed concrete sextuples.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple $(0,1,0,1,3,1)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of the numerator fold and the explicit table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges the universal claim by fin_cases on all six indices, landing on these pointwise kernel facts.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint $M_2$ TT kernel in 4D Regge calculus: it replaces a folded coupling sum by a sparse explicit integer table, scaled by eight. It does not itself touch the forcing chain (T0–T8), $\phi$, or the RCL; it is pure discrete-kernel arithmetic supporting the continuum gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.