e_110310
plain-language theorem explainer
For the six Fin-4 indices (1,1,0,3,1,0), the summed midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 4^6 case certificates. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=1,b=1,c=0,d=3,i=1,j=0$ in $\mathrm{Fin}\,4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $\mathrm{m2Num}$ is defined by folding a coupling list: it accumulates every contribution $\mathrm{contrib},t,a,b,c,d,i,j$ over $t\in\mathrm{couplingZList}$. The comparison target $\mathrm{explicitZ}$ is a closed-form pattern-matched integer table (entries such as $4$, $-2$, and so on for selected index patterns).
The module is chunk 5 of a 256-way kernel-decide partition of the identity $\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$. Each chunk discharges a block of concrete sextuples so the global assembly can finish by exhaustive $\mathrm{fin_cases}$ without re-evaluating the fold at proof time.
Upstream, only the two definitions are needed: the fold that builds $\mathrm{m2Num}$ and the table that defines $\mathrm{explicitZ}$. No analytic lemma intervenes; the equality is pure integer arithmetic on fixed indices.
proof idea
One-line proof by decide. Lean reduces both sides at the concrete sextuple $(1,1,0,3,1,0)$: the left-hand fold over couplingZList evaluates to an integer, the right-hand side is $8$ times the matching explicitZ clause (or the default), and the kernel checks equality. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
This certificate is one leaf in the case tree that proves m2Num_eq_eight_explicitZ: $\forall a,b,c,d,i,j:\mathrm{Fin},4,;\mathrm{m2Num},a,b,c,d,i,j=8\cdot\mathrm{explicitZ},a,b,c,d,i,j$. That global identity is the numerical core of the Regge exact-midpoint M2TT 4D kernel certification in the Gravity analysis stack.
Within Recognition Science gravity work, the midpoint identity constrains discrete curvature contributions that feed continuum limits and effective Newtonian potentials. The chunking strategy (256 kernel decides) keeps each certificate tiny and machine-checkable while the assembler stitches them by nested fin_cases. The declaration itself closes no open physics question; it is pure bookkeeping that makes the assembled equality hold without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.