e_201023
plain-language theorem explainer
Pointwise identity: the m2 numerator kernel at multi-index (2,0,1,0,2,3) equals eight times the explicit Z table entry there. Gravity analysts cite it as one cell of the 4D Regge midpoint m2=8Z certification. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,0,1,0,2,3)$ with each slot in $\{0,1,2,3\}$, the folded coupling numerator $m_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer table $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer kernels on six Fin 4 indices are compared. The numerator m2Num is the fold of a fixed coupling list: each term contributes an integer contrib and the accumulator starts at 0. The comparison target explicitZ is a closed-form case table on the same six indices (sample clauses include values 4, -2, and so on).
This module is chunk 8 of the exhaustive pointwise certification that m2Num = 8 · explicitZ at every multi-index. The local setting is pure integer equality after full evaluation of both sides; no continuum limit or physical units enter the statement.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six indices are substituted into the fold definition of m2Num and the case table explicitZ, so the kernel discharges the equality with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all six Fin 4 arguments and proves it by nested fin_cases, invoking one chunk lemma per cell. That global equality is the algebraic backbone of the Regge midpoint m2–TT identity certification in the gravity analysis stack. Within Recognition Science this sits in the discrete geometric bookkeeping for gravitational kernels, not in the T0–T8 forcing chain itself; it is infrastructure that keeps the 4D midpoint identities machine-checked rather than hand-tabulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.