e_301022
plain-language theorem explainer
Pointwise identity: the Regge midpoint m2 numerator at multi-index (3,0,1,0,2,2) equals eight times the explicit Z-table entry. Gravity analysts cite it when assembling the full 4D kernel identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(3,0,1,0,2,2)$ in $(\mathbb{F}_4)^6$, the summed 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 12 of a 256-case kernel certification that the 4D Regge midpoint m2 numerator equals eight times an explicit integer table. The ambient setting is discrete gravity analysis: index sextuples range over $\mathbb{F}_4$, and equalities are decided by exact integer arithmetic rather than symbolic cancellation.
Upstream, $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer contrib at the six indices, summed from zero. The companion table explicitZ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on diagonal and off-diagonal patterns).
The local claim is one concrete sextuple in that table-versus-sum comparison. Sibling lemmas cover the other index combinations in the same chunk style.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are fixed at $(3,0,1,0,2,2)$. Lean’s decision procedure evaluates the fold that defines the numerator and the pattern match that defines the explicit table, then checks integer equality. No lemmas beyond the two defining defs are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies over all six indices and discharges the identity by exhaustive fin_cases; each case lands on a chunk lemma of this form. Without the pointwise facts, the assembly cannot close.
In the Recognition gravity stack this certifies an exact algebraic identity in the 4D Regge midpoint kernel (TT sector), not an asymptotic or floating-point check. It is infrastructure for the discrete curvature/mass-side bookkeeping that later meets continuum limits, rather than a forcing-chain (T0–T8) step itself. Closing all 256 decides removes a scaffolding surface in the midpoint m2 analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.