e_003100
plain-language theorem explainer
For the multi-index (0,0,3,1,0,0), the folded coupling numerator equals eight times the explicit integer table entry. Gravity analysts cite it as one of the 256 kernel cells that assemble the full m2Num = 8·explicitZ identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,0,3,1,0,0)$ in $(\mathrm{Fin}\,4)^6$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit table value $Z(a,b,c,d,i,j)$.
background
This module is one cell of the 4D Regge midpoint $M_2$ TT-identity certification. The local claim is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on a fixed multi-index, proved by kernel decision rather than by algebraic expansion.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $\mathrm{explicitZ}$ is a closed integer table on $(\mathrm{Fin},4)^6$, with nonzero pattern entries such as $4$ on diagonal-type slots and $-2$ on selected off-diagonal slots.
Chunk 0 packages 256 such pointwise equalities. Downstream assembly quantifies over all six $\mathrm{Fin},4$ indices by exhaustive case split.
proof idea
One-line proof: decide. Both sides reduce to concrete integers once the six indices are fixed at $(0,0,3,1,0,0)$, so the kernel checks integer equality with no further lemmas. No unfolding of the fold or of the table cases is written by hand.
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\cdot Z$ and discharges the universal claim by fin_cases on each coordinate. That global identity is the algebraic core of the Regge exact-midpoint $M_2$ TT certification in four dimensions: it replaces a summed coupling expression by an eightfold multiple of a sparse explicit table, making later curvature and deficit identities cheap to evaluate.
Within Recognition gravity analysis this is bookkeeping, not a new physical law. It sits under the discrete geometric layer that supports continuum limits and effective Newtonian recovery, not under the T0–T8 forcing chain itself. Closing all 256 cells removes a scaffolding surface on the midpoint identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.