e_023022
plain-language theorem explainer
Pointwise identity: the Regge midpoint numerator at multi-index (0,2,3,0,2,2) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full 4D kernel certificate m2Num = 8·explicitZ. Proof is a single kernel decide on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,3,0,2,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(0,2,3,0,2,2)=8\,Z(0,2,3,0,2,2)$.
background
This module is chunk 2 of a 256-way split of the 4D Regge midpoint kernel identity $N=8Z$. The ambient setting is discrete gravity analysis: six indices in $\mathrm{Fin},4$ label pairs of edge/face data on a 4-simplex skeleton.
The numerator $N=\mathrm{m2Num}$ 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 table $Z=\mathrm{explicitZ}$ is a hand-written integer function on the same six indices (sample clauses: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and so on).
The local claim is only the single tuple $(0,2,3,0,2,2)$; siblings cover the rest of the chunk.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are literals, so the kernel equality checker discharges $N=8Z$ with no lemmas or case splits inside this declaration.
why it matters
Feeds the assembly theorem $\forall a,b,c,d,i,j,,N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ in ReggeExactMidpointM2TTIdentity4DM2NumAssemble, which glues all 256 pointwise certificates (via exhaustive fin-cases on the six indices). That global identity is the algebraic core of the exact midpoint M2 TT kernel certificate for 4D Regge calculus in the Gravity analysis stack. It is bookkeeping, not a new physical law: it locks the folded coupling sum to the closed integer table used downstream in curvature and mass-gap numerics. No T0–T8 forcing step is touched; the link is infrastructure for discrete gravity identities inside Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.