e_021120
plain-language theorem explainer
For the six-index tuple (0,2,1,1,2,0) on Fin 4, the folded Regge midpoint numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts cite it as one atomic case in the 4D M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,1,2,0)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $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 midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator m2Num folds a fixed coupling list, summing a local contribution at each term for the given multi-index. The comparison target explicitZ is a sparse pattern-matched table of small integers (entries such as 4, -2, and so on on the diagonal and near-diagonal slots).
The module is chunk 2 of a 256-case kernel certification that m2Num = 8 · explicitZ pointwise. The local setting is pure finite enumeration: every index runs over Fin 4, so the identity is a finite family of integer equations, split across chunk files for compile-time control.
Upstream, m2Num and explicitZ are the two sides of the claimed equality; no analytic continuum limit is invoked at this layer.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted: m2Num evaluates the fold of coupling contributions, explicitZ hits its pattern match (or the default), and the kernel checks the resulting integer equality m2Num = 8 * explicitZ for this single tuple.
why it matters
This declaration is one atomic witness in the exhaustive case split that builds m2Num_eq_eight_explicitZ, the pointwise theorem ∀ (a b c d i j : Fin 4), m2Num a b c d i j = 8 * explicitZ a b c d i j, assembled by fin_cases on all six indices. That global identity is the algebraic core of the Regge exact-midpoint M2–TT certification in 4D gravity analysis inside the monolith.
Within Recognition Science gravity work, such kernel identities underwrite discrete curvature bookkeeping on the eight-tick / D = 3 side of the forcing chain, keeping the midpoint numerator tied to an explicit sparse Z table rather than an opaque sum. The chunk exists only to keep the 256 decides modular; the scientific claim lives at the assembled forall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.