e_023322
plain-language theorem explainer
Pointwise check that the Regge midpoint m2 numerator equals eight times the explicit Z-table entry at multi-index (0,2,3,3,2,2). Gravity analysts cite it as one of the 256 kernel cells glued by the full m2Num=8·Z assembly. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,3,3,2,2)$ in $(\mathrm{Fin}\,4)^6$, 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
This module is chunk 2 of a 256-cell kernel certification that the midpoint Regge $m_2$ numerator coincides with eight times a closed-form integer table. The ambient setting is 4D Regge calculus on a midpoint-evaluated TT sector: discrete curvature couplings are reduced to finite sums over a fixed coupling list.
The numerator $m_2^{\mathrm{num}}$ is defined by folding couplingZList and summing a local contribution at each six-index slot. The comparison object $Z$ is an explicit pattern-matched integer table on $(\mathrm{Fin},4)^6$ (sample clauses give values such as $4$, $-2$, etc.). The identity claimed cellwise is $m_2^{\mathrm{num}}=8Z$.
Upstream, only those two definitions are needed: the fold that builds the numerator and the table that supplies the right-hand side.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(0,2,3,3,2,2)$ in the integer ring and checks equality. No algebraic rewriting or named lemmas beyond the two defining constants; the kernel simply reduces the fold and the table lookup to numerals and compares them.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on all six $\mathrm{Fin},4$ indices. Each chunk theorem such as this one discharges one concrete cell so the assembler can chain the cases without re-deciding the whole kernel inline.
In the Recognition gravity stack this closes a discrete midpoint identity used when matching Regge curvature bookkeeping to the continuum TT sector. It is pure finite combinatorics: no continuum limit, no dynamical field equations, and no appeal to the T0–T8 forcing chain beyond sitting inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.