e_112103
plain-language theorem explainer
For the six-index slot (1,1,2,1,0,3) on Fin 4, the folded Regge numerator coupling equals eight times the explicit kernel table entry. Gravity analysts certifying the 4D midpoint M2TT identity cite this as one atomic kernel cell. The proof is a single `decide` on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the numerator coupling $m_2^{\mathrm{num}}(1,1,2,1,0,3)$ equals $8\,Z(1,1,2,1,0,3)$, where $Z$ is the explicit integer kernel and $m_2^{\mathrm{num}}$ is the fold of all coupling contributions at that multi-index.
background
This module sits in the 4D Regge exact-midpoint analysis: one must show that a folded numerator built from coupling contributions agrees with eight times a closed-form integer kernel on every six-tuple of face indices in $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList, accumulating each term's contribution at the given indices. The comparison table explicitZ is a pattern-matched integer function on the same six Fin 4 arguments (typical values $\pm 2,,4$, and zero off the listed patterns).
The local setting is chunk 5 of a 256-cell kernel decide sweep: each cell is an equality at one concrete multi-index, later assembled into the universal statement.
proof idea
One-line computational certificate: by decide. Both sides reduce to concrete Int values (the fold on the left, the pattern match on the right), and the kernel checks equality. No lemmas beyond the definitions of m2Num and explicitZ are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases on all six indices. That universal identity is the algebraic core of the Regge exact-midpoint M2TT certification in 4D gravity analysis inside the monolith.
In the broader Recognition stack this is bookkeeping infrastructure for discrete curvature/action identities, not a forcing-chain landmark (T5–T8) or an RCL step. It closes one cell of the kernel table so the parent no longer depends on an unproven case split at this slot.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.