e_201110
plain-language theorem explainer
Pointwise identity: the midpoint Regge m₂ numerator at multi-index (2,0,1,1,1,0) equals eight times the explicit Z-table entry. Gravity analysts cite it when assembling the global m₂Num = 8·explicitZ certificate over Fin 4⁶. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,1,1,0)$ 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
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib and the fold starts at 0. The comparison target explicitZ is a sparse case table of small integers (entries such as $4$, $-2$, and so on) on the same six-index domain.
The local module is chunk 8 of a 256-way split of the kernel: each chunk discharges a block of concrete multi-indices by decision procedure, aiming at the schematic identity $m_2^{\mathrm{num}}=8\cdot Z$ everywhere on $(\mathrm{Fin},4)^6$.
Upstream, only the definitions of the fold and the table are required; no analytic lemma is invoked at a single point.
proof idea
One-line proof: decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are fixed at $(2,0,1,1,1,0)$, so the kernel closes the equality with no lemmas, rewrites, or case splits inside this declaration.
why it matters
This is one tile in the 256-point cover that 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 proves it by exhaustive fin_cases on the six indices. Without the pointwise chunk facts, the assembly cannot discharge every residual goal.
In the broader Gravity/Regge strand of Recognition Science, the identity certifies that the midpoint discrete curvature numerator matches an explicit closed-form table up to the universal factor 8, a bookkeeping step toward exact 4D midpoint identities rather than a forcing-chain (T0–T8) landmark. It closes no open physics conjecture by itself; it removes one concrete obstruction in the kernel certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.