e_033112
plain-language theorem explainer
Pointwise identity: the midpoint Regge numerator coupling at multi-index (0,3,3,1,1,2) equals eight times the explicit kernel value Z at those indices. Gravity analysts cite it as one cell of the 4D M2–TT kernel check. Closed by a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,1,1,2)$ in $\mathrm{Fin}\,4$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator coupling $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes via a local contrib and the accumulator starts at $0$. The comparison target is explicitZ, a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and defaults).
The module is chunk 3 of a 256-way kernel split whose sole job is to certify $m_2^{\mathrm{num}}=8\cdot Z$ at every index tuple. This declaration is the cell for $(0,3,3,1,1,2)$. Upstream, only the two definitions are needed: the fold that builds $m_2^{\mathrm{num}}$ and the table that defines $Z$.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six indices are fixed: the fold over couplingZList evaluates fully, explicitZ matches its pattern (or default), and Lean’s kernel checks the resulting integer equality $m_2^{\mathrm{num}}=8Z$. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all $a,b,c,d,i,j:\mathrm{Fin},4$ by exhaustive fin_cases. That global equality is the certified bridge between the folded numerator coupling and the closed-form kernel table in the Regge midpoint M2–TT identity. Without each chunk cell (including this one), the 4D gravity kernel certificate does not close. Landmark link is local to the gravity analysis stack rather than T0–T8; it is infrastructure for the discrete curvature/mass side of the RS gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.